1 /-
2 Copyright (c) 2017 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 Cofinality on ordinals, regular cardinals.
7 -/
8 import set_theory.ordinal
src └────────────────┘
9 noncomputable theory
10
11 open function cardinal set
12 open_locale classical
13
14 universes u v w
15 variables {α : Type*} {r : α → α → Prop}
16
17 namespace order
18 /-- Cofinality of a reflexive order `≼`. This is the smallest cardinality
19 of a subset `S : set α` such that `∀ a, ∃ b ∈ S, a ≼ b`. -/
20 def cof (r : α → α → Prop) [is_refl α r] : cardinal :=
id ┴ ┴ └─────┘ ┴ ┴ └──────┘
src └─────┘ └──────┘
typ ┴ ┴ └─────┘ ┴ ┴ └──────┘
doc └──────┘
21 @cardinal.min {S : set α // ∀ a, ∃ b ∈ S, r a b}
id └──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────────┘ ┴ └─┘ ┴ ┴
typ └──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──────────┘
22 ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
id └──────┘ ┴ ┴ ┴ └──┘
src └──────┘ ┴ └──┘
typ └──────┘ ┴ ┴ ┴ └──┘
23 (λ S, mk S)
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
24
25 lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) :
id ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
26 order.cof r ≤ mk S :=
id └───────┘ ┴ ┴ └┘ ┴
src └───────┘ ┴ └┘
typ └───────┘ ┴ ┴ └┘ ┴
doc └───────┘ └┘
27 le_trans (cardinal.min_le _ ⟨S, h⟩) (le_refl _)
id └──────┘ └─────────────┘ ┴ ┴ └─────┘
src └──────┘ └─────────────┘ └─────┘
typ └──────┘ └─────────────┘ ┴ ┴ └─────┘
28
29 lemma le_cof {r : α → α → Prop} [is_refl α r] (c : cardinal) :
id ┴ ┴ └─────┘ ┴ ┴ └──────┘
src └─────┘ └──────┘
typ ┴ ┴ └─────┘ ┴ ┴ └──────┘
doc └──────┘
30 c ≤ order.cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ mk S :=
id ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ └┘
typ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └───────┘ └┘
31 by { rw [order.cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }
id └───────┘ └─────────────┘ ┴
src └──┘└───────┘└┘└─────────────┘┴ └────┘ └──────┘ ┴ └┘ └─┘ └──┘ └┘ └─┘ ┴ └─┘
typ └──┘└───────┘└┘└─────────────┘┴ └────┘ └──────┘ ┴ └┘ └─┘ └──┘ └┘┴└─┘ ┴ └─┘
doc └──┘└───────┘└┘ ┴ └────┘ └──────┘ ┴ └┘ └─┘ └──┘ └┘ └─┘ ┴ └─┘
txt └──┘ └┘ ┴ └────┘ └──────┘ ┴ └┘ └─┘ └──┘ └┘ └─┘ ┴ └─┘
par └──┘ └┘ ┴ └────┘ └──────┘ ┴ └┘ └─┘ └──┘ └┘ └─┘ ┴ └─┘
pid └┘ └┘ ┴ ┴ └──────┘ ┴ └┘ └─┘ └──┘ └┘ └─┘ ┴ └┘┴
st └──────────────┘└───────────────┘└─────────────────────────────────────────────┘└┘
32
33 end order
34
35 theorem order_iso.cof.aux {α : Type u} {β : Type v} {r s}
36 [is_refl α r] [is_refl β s] (f : r ≃o s) :
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
src └─────┘ └─────┘ └┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
doc └┘
37 cardinal.lift.{u (max u v)} (order.cof r) ≤
id └───────────┘ └───────┘ ┴ ┴
src └───────────┘ └───────┘ ┴
typ └───────────┘ └───────┘ ┴ ┴
doc └───────────┘ └───────┘
38 cardinal.lift.{v (max u v)} (order.cof s) :=
id └───────────┘ └───────┘ ┴
src └───────────┘ └───────┘
typ └───────────┘ └───────┘ ┴
doc └───────────┘ └───────┘
39 begin
st └─────
40 rw [order.cof, order.cof, lift_min, lift_min, cardinal.le_min],
id └───────┘ └───────┘ └──────┘ └──────┘ └─────────────┘
src └──┘└───────┘└┘└───────┘└┘└──────┘└┘└──────┘└┘└─────────────┘┴
typ └──┘└───────┘└┘└───────┘└┘└──────┘└┘└──────┘└┘└─────────────┘┴
doc └──┘└───────┘└┘└───────┘└┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ──────────────┘└─────────┘└────────┘└────────┘└───────────────┘└──
41 intro S, cases S with S H, simp [(∘)],
id ┴ ┴
src └─────┘ └────┘ └───────┘ └────┘┴└─┘
typ └─────┘ └────┘┴└───────┘ └────┘┴└─┘
doc └─────┘ └────┘ └───────┘ └────┘ └─┘
txt └─────┘ └────┘ └───────┘ └────┘ └─┘
par └─────┘ └────┘ └───────┘ └────┘ └─┘
pid └┘ ┴ └───────┘ ┴┴ └─┘
st ────────┘└────────────────┘└──────────┘└─
42 refine le_trans (min_le _ _) _,
id └──────┘ └────┘
src └─────┘└──────┘┴ └────┘└─────┘
typ └─────┘└──────┘┴ └────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ───────────────────────────────┘└─
43 { exact ⟨f ⁻¹' S, λ a,
id └─┘ ┴
src └────┘ ┴└─┘┴ └┘ └───
typ └────┘ ┴└─┘┴┴└┘ └───
doc └────┘ ┴└─┘┴ └┘ └───
txt └────┘ ┴ ┴ └┘ └───
par └────┘ ┴ ┴ └┘ └───
pid ┴ ┴ ┴ └┘ └───
st ───┘└────────────────────
44 let ⟨b, bS, h⟩ := H (f a) in ⟨f.symm b, by simp [bS, f.ord', h,
id ┴ ┴ ┴ └────┘ └┘ ┴
src ───┘ ┴ └┘ └┘ └───┘ ┴ ┴ └───┘ └────┘┴ └┘ ┴└────┘ └┘ └┘ └─
typ ───┘ ┴ ┴└┘ └┘ └───┘┴┴ ┴┴ └───┘ └────┘┴ └┘ ┴└────┘└┘└┘└────┘└┘┴└─
doc ───┘ ┴ └┘ └┘ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴└────┘ └┘ └┘ └─
txt ───┘ ┴ └┘ └┘ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴└────┘ └┘ └┘ └─
par ───┘ ┴ └┘ └┘ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴└────┘ └┘ └┘ └─
pid ───┘ ┴ └┘ └┘ └───┘ ┴ ┴ └───┘ ┴ └┘ └─────┘ └┘ └┘ └─
st ─────────────────────────────────────────────┘└─────────────────────
45 -coe_fn_coe_base, -coe_fn_coe_trans, principal_seg.coe_coe_fn', initial_seg.coe_coe_fn]⟩⟩ },
id └───────────────────────┘ └────────────────────┘
src ──────────────────────────────────────────┘└───────────────────────┘└┘└────────────────────┘┴└─┘
typ ──────────────────────────────────────────┘└───────────────────────┘└┘└────────────────────┘┴└─┘
doc ──────────────────────────────────────────┘ └┘ ┴└─┘
txt ──────────────────────────────────────────┘ └┘ ┴└─┘
par ──────────────────────────────────────────┘ └┘ ┴└─┘
pid ──────────────────────────────────────────┘ └┘ └─┘┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─┘└┘└
46 { exact lift_mk_le.{u v (max u v)}.2
id └────────┘
src └────┘└────────┘└──────────────────
typ └────┘└────────┘└──────────────────
doc └────┘ └──────────────────
txt └────┘ └──────────────────
par └────┘ └──────────────────
pid ┴ └──────────────────
st ───────────────────────────────────────
47 ⟨⟨λ ⟨x, h⟩, ⟨f x, h⟩, λ ⟨x, h₁⟩ ⟨y, h₂⟩ h₃,
id ┴ ┴ ┴
src ───┘ └┘ └┘ └─┘ ┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
typ ───┘ └┘┴└┘┴└─┘ ┴┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
doc ───┘ └┘ └┘ └─┘ ┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
txt ───┘ └┘ └┘ └─┘ ┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
par ───┘ └┘ └┘ └─┘ ┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
pid ───┘ └┘ └┘ └─┘ ┴ └┘ └─┘ └┘ └┘ └─┘ └┘ └─────
st ────────────────────────────────────────────────
48 by congr; injection h₃ with h'; exact f.to_equiv.injective h'⟩⟩ }
id └┘ └──────────────────┘ └┘
src ─────┘ ┴└───┘└┘└────────┘ └──────┘└──────┘└──────────────────┘┴ └─┘
typ ─────┘ ┴└───┘└┘└────────┘└┘└──────┘└──────┘└──────────────────┘┴└┘└─┘
doc ─────┘ ┴ └┘└────────┘ └──────┘└──────┘ ┴ └─┘
txt ─────┘ ┴└───┘└┘└────────┘ └──────┘└──────┘ ┴ └─┘
par ─────┘ ┴└───┘└┘└────────┘ └──────┘└──────┘ ┴ └─┘
pid ─────┘ └────────────────┘ └──────────────┘ ┴ └┘┴
st ───────┘└─────────────────────────────────────────────────────────┘└─┘└─
49 end
st ──┘
50
51 theorem order_iso.cof {α : Type u} {β : Type v} {r s}
52 [is_refl α r] [is_refl β s] (f : r ≃o s) :
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
src └─────┘ └─────┘ └┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴
doc └┘
53 cardinal.lift.{u (max u v)} (order.cof r) =
id └───────────┘ └───────┘ ┴ ┴
src └───────────┘ └───────┘ ┴
typ └───────────┘ └───────┘ ┴ ┴
doc └───────────┘ └───────┘
54 cardinal.lift.{v (max u v)} (order.cof s) :=
id └───────────┘ └───────┘ ┴
src └───────────┘ └───────┘
typ └───────────┘ └───────┘ ┴
doc └───────────┘ └───────┘
55 le_antisymm (order_iso.cof.aux f) (order_iso.cof.aux f.symm)
id └─────────┘ └───────────────┘ ┴ └───────────────┘ ┴└───┘
src └─────────┘ └───────────────┘ └───────────────┘ └───┘
typ └─────────┘ └───────────────┘ ┴ └───────────────┘ ┴└───┘
56
57 def strict_order.cof (r : α → α → Prop) [h : is_irrefl α r] : cardinal :=
id ┴ ┴ └───────┘ ┴ ┴ └──────┘
src └───────┘ └──────┘
typ ┴ ┴ └───────┘ ┴ ┴ └──────┘
doc └──────┘
58 @order.cof α (λ x y, ¬ r y x) ⟨h.1⟩
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └───────┘
59
60 namespace ordinal
61
62 /-- Cofinality of an ordinal. This is the smallest cardinal of a
63 subset `S` of the ordinal which is unbounded, in the sense
64 `∀ a, ∃ b ∈ S, ¬(b > a)`. It is defined for all ordinals, but
65 `cof 0 = 0` and `cof (succ o) = 1`, so it is only really
66 interesting on limit ordinals (when it is an infinite cardinal). -/
67 def cof (o : ordinal.{u}) : cardinal.{u} :=
id └─────┘ └──────┘
src └─────┘ └──────┘
typ └─────┘ └──────┘
doc └─────┘ └──────┘
68 quot.lift_on o (λ ⟨α, r, _⟩, by exactI strict_order.cof r) $
id └──────────┘ ┴ ┴ └──────────────┘ ┴
src └──────────┘ └─────┘└──────────────┘┴
typ └──────────┘ ┴ ┴ └─────┘└──────────────┘┴┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴ ┴
st └────────────────────────┘
69 λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩, begin resetI,
id ┴ ┴ ┴
src └────┘
typ ┴ ┴ ┴ └────┘
doc └────┘
txt └────┘
par └────┘
st └─────────────
70 show strict_order.cof r = strict_order.cof s,
id ┴ ┴ └──────────────┘ ┴
src └───┘ ┴ ┴┴┴└──────────────┘┴
typ └───┘ ┴┴┴┴┴└──────────────┘┴┴
doc └───┘ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────┘└─
71 refine cardinal.lift_inj.1 (@order_iso.cof _ _ _ _ ⟨_⟩ ⟨_⟩ _),
id └───────────────┘ └───────────┘
src └─────┘└───────────────┘└─┘ └───────────┘└───────┘ └─┘ └───┘
typ └─────┘└───────────────┘└─┘ └───────────┘└───────┘ └─┘ └───┘
doc └─────┘ └─┘ └───────┘ └─┘ └───┘
txt └─────┘ └─┘ └───────┘ └─┘ └───┘
par └─────┘ └─┘ └───────┘ └─┘ └───┘
pid ┴ └─┘ └───────┘ └─┘ └───┘
st ──────────────────────────────────────────────────────────────┘└─
72 exact ⟨f, λ a b, not_congr hf⟩,
id ┴ └───────┘ └┘
src └────┘ └┘ └────┘└───────┘┴ ┴
typ └────┘ ┴└┘ └────┘└───────┘┴└┘┴
doc └────┘ └┘ └────┘ ┴ ┴
txt └────┘ └┘ └────┘ ┴ ┴
par └────┘ └┘ └────┘ ┴ ┴
pid ┴ └┘ └────┘ ┴ ┴
st ───────────────────────────────┘└─
73 end
st ──┘
74
75 lemma cof_type (r : α → α → Prop) [is_well_order α r] : (type r).cof = strict_order.cof r := rfl
id ┴ ┴ └───────────┘ ┴ ┴ └──┘ ┴ └─┘ ┴ └──────────────┘ ┴ └─┘
src └───────────┘ └──┘ └─┘ ┴ └──────────────┘ └─┘
typ ┴ ┴ └───────────┘ ┴ ┴ └──┘ ┴ └─┘ ┴ └──────────────┘ ┴ └─┘
doc └───────────┘ └──┘ └─┘
76
77 theorem le_cof_type [is_well_order α r] {c} : c ≤ cof (type r) ↔
id └───────────┘ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴
src └───────────┘ ┴ └─┘ └──┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴
doc └───────────┘ └─┘ └──┘
78 ∀ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) → c ≤ mk S :=
id └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴ ┴ └┘
typ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
79 by dsimp [cof, strict_order.cof, order.cof, type, quotient.mk, quot.lift_on];
id └─┘ └──────────────┘ └───────┘ └──┘ └─────────┘ └──────────┘
src └─────┘└─┘└┘└──────────────┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘┴
typ └─────┘└─┘└┘└──────────────┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘┴
doc └─────┘└─┘└┘ └┘└───────┘└┘└──┘└┘ └┘ ┴
txt └─────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────────────────────────────────
80 rw [cardinal.le_min, subtype.forall]; refl
id └─────────────┘ └────────────┘
src └──┘└─────────────┘└┘└────────────┘┴ └────
typ └──┘└─────────────┘└┘└────────────┘┴ └────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st ──────┘└─────────────┘└──────────────┘┴└──────
81
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
82 theorem cof_type_le [is_well_order α r] (S : set α) (h : ∀ a, ∃ b ∈ S, ¬ r b a) :
id └───────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────────┘ └─┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────────┘
83 cof (type r) ≤ mk S :=
id └─┘ └──┘ ┴ ┴ └┘ ┴
src └─┘ └──┘ ┴ └┘
typ └─┘ └──┘ ┴ ┴ └┘ ┴
doc └─┘ └──┘ └┘
84 le_cof_type.1 (le_refl _) S h
id └─────────┘┴ └─────┘ ┴ ┴
src └─────────┘┴ └─────┘
typ └─────────┘┴ └─────┘ ┴ ┴
85
86 theorem lt_cof_type [is_well_order α r] (S : set α) (hl : mk S < cof (type r)) :
id └───────────┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
src └───────────┘ └─┘ └┘ ┴ └─┘ └──┘
typ └───────────┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
doc └───────────┘ └┘ └─┘ └──┘
87 ∃ a, ∀ b ∈ S, r b a :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
88 not_forall_not.1 $ λ h, not_le_of_lt hl $ cof_type_le S (λ a, not_ball.1 (h a))
id └────────────┘┴ ┴ └──────────┘ └┘ └─────────┘ ┴ ┴ └──────┘┴ ┴ ┴
src └────────────┘┴ └──────────┘ └─────────┘ └──────┘┴
typ └────────────┘┴ ┴ └──────────┘ └┘ └─────────┘ ┴ ┴ └──────┘┴ ┴ ┴
89
90 theorem cof_eq (r : α → α → Prop) [is_well_order α r] :
id ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
91 ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ mk S = cof (type r) :=
id ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └──┘
typ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
doc └┘ └─┘ └──┘
92 begin
st └─────
93 have : ∃ i, cof (type r) = _,
id ┴ ┴ └─┘ └──┘ ┴ ┴
src └─────┘┴└┘┴┴└─┘┴ └──┘┴ └┘┴└┘
typ └─────┘┴└┘┴┴└─┘┴ └──┘┴┴└┘┴└┘
doc └─────┘ └┘ ┴└─┘┴ └──┘┴ └┘ └┘
txt └─────┘ └┘ ┴ ┴ ┴ └┘ └┘
par └─────┘ └┘ ┴ ┴ ┴ └┘ └┘
pid └───┘└┘ └┘ ┴ ┴ ┴ └┘ └┘
st ─────────────────────────────┘└─
94 { dsimp [cof, order.cof, type, quotient.mk, quot.lift_on],
id └─┘ └───────┘ └──┘ └─────────┘ └──────────┘
src └─────┘└─┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘┴
typ └─────┘└─┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘┴
doc └─────┘└─┘└┘└───────┘└┘└──┘└┘ └┘ ┴
txt └─────┘ └┘ └┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st ───┘└─────────────────────────────────────────────────────┘└─
95 apply cardinal.min_eq },
id └─────────────┘
src └────┘└─────────────┘┴
typ └────┘└─────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────┘└┘└
96 exact let ⟨⟨S, hl⟩, e⟩ := this in ⟨S, hl, e.symm⟩,
id ┴ └┘ ┴ └──┘ └───┘
src └────┘ ┴ └┘ └─┘ └───┘ └──┘ └┘ └┘ └───┘┴
typ └────┘ ┴ ┴└┘└┘└─┘┴└───┘└──┘└──┘ └┘ └┘ └───┘┴
doc └────┘ ┴ └┘ └─┘ └───┘ └──┘ └┘ └┘ ┴
txt └────┘ ┴ └┘ └─┘ └───┘ └──┘ └┘ └┘ ┴
par └────┘ ┴ └┘ └─┘ └───┘ └──┘ └┘ └┘ ┴
pid ┴ ┴ └┘ └─┘ └───┘ └──┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────┘└─
97 end
st ──┘
98
99 theorem ord_cof_eq (r : α → α → Prop) [is_well_order α r] :
id ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
100 ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ type (subrel r S) = (cof (type r)).ord :=
id ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ ┴ └─┘ └──┘ └─┘
typ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘
doc └──┘ └────┘ └─┘ └──┘ └─┘
101 let ⟨S, hS, e⟩ := cof_eq r, ⟨s, _, e'⟩ := cardinal.ord_eq S,
id └─┘ ┴ └────┘ ┴ ┴ └─────────────┘
src └────┘ └─────────────┘
typ └─┘ ┴ └────┘ ┴ ┴ └─────────────┘
102 T : set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a} in
id └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
103 begin
st └─────
104 resetI, suffices,
src └────┘ └──────┘
typ └────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid └──────┘
st ─────────────────┘└─
105 { refine ⟨T, this,
src └─────┘ └┘ └─
typ └─────┘ └┘ └─
doc └─────┘ └┘ └─
txt └─────┘ └┘ └─
par └─────┘ └┘ └─
pid ┴ └┘ └─
st ───┘└────────────────
106 le_antisymm _ (cardinal.ord_le.2 $ cof_type_le T this)⟩,
id └─────────┘ └─────────────┘ └─────────┘ ┴ └──┘
src ─────┘└─────────┘└─┘ └─────────────┘└─┘ ┴└─────────┘┴ ┴ └┘
typ ─────┘└─────────┘└─┘ └─────────────┘└─┘ ┴└─────────┘┴┴┴└──┘└┘
doc ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘
txt ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘
par ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘
pid ─────┘ └─┘ └─┘ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────┘└─
107 rw [← e, e'],
id ┴ └┘
src └────┘ └┘ ┴
typ └────┘┴└┘└┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ──────────┘└──┘└──
108 refine type_le'.2 ⟨order_embedding.of_monotone
id └──────┘ └─────────────────────────┘
src └─────┘└──────┘└─┘ └─────────────────────────┘└
typ └─────┘└──────┘└─┘ └─────────────────────────┘└
doc └─────┘ └─┘ └─────────────────────────┘└
txt └─────┘ └─┘ └
par └─────┘ └─┘ └
pid ┴ └─┘ └
st ───────────────────────────────────────────────────
109 (λ a, ⟨a, let ⟨aS, _⟩ := a.2 in aS⟩) (λ a b h, _)⟩,
id └┘
src ─────┘ └──┘ └┘ ┴ └──────┘ └────┘ └─┘ └─────────┘
typ ─────┘ └──┘ └┘ ┴ └┘└──────┘ └────┘ └─┘ └─────────┘
doc ─────┘ └──┘ └┘ ┴ └──────┘ └────┘ └─┘ └─────────┘
txt ─────┘ └──┘ └┘ ┴ └──────┘ └────┘ └─┘ └─────────┘
par ─────┘ └──┘ └┘ ┴ └──────┘ └────┘ └─┘ └─────────┘
pid ─────┘ └──┘ └┘ ┴ └──────┘ └────┘ └─┘ └─────────┘
st ───────────────────────────────────────────────────────┘└─
110 rcases a with ⟨a, aS, ha⟩, rcases b with ⟨b, bS, hb⟩,
id ┴ ┴
src └─────┘ └───────────────┘ └─────┘ └───────────────┘
typ └─────┘┴└───────────────┘ └─────┘┴└───────────────┘
doc └─────┘ └───────────────┘ └─────┘ └───────────────┘
txt └─────┘ └───────────────┘ └─────┘ └───────────────┘
par └─────┘ └───────────────┘ └─────┘ └───────────────┘
pid ┴ └───────────────┘ ┴ └───────────────┘
st ────────────────────────────┘└─────────────────────────┘└─
111 change s ⟨a, _⟩ ⟨b, _⟩,
id ┴ ┴ ┴
src └─────┘ ┴ └───┘ └──┘
typ └─────┘┴┴ ┴└───┘ ┴└──┘
doc └─────┘ ┴ └───┘ └──┘
txt └─────┘ ┴ └───┘ └──┘
par └─────┘ ┴ └───┘ └──┘
pid ┴ ┴ └───┘ └──┘
st ─────────────────────────┘└─
112 refine ((trichotomous_of s _ _).resolve_left (λ hn, _)).resolve_left _,
id └─────────────┘ ┴
src └─────┘ └─────────────┘┴ └─────────────────┘ └─────────────────────┘
typ └─────┘ └─────────────┘┴┴└─────────────────┘ └─────────────────────┘
doc └─────┘ ┴ └─────────────────┘ └─────────────────────┘
txt └─────┘ ┴ └─────────────────┘ └─────────────────────┘
par └─────┘ ┴ └─────────────────┘ └─────────────────────┘
pid ┴ ┴ └─────────────────┘ └─────────────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
113 { exact asymm h (ha _ hn) },
id └───┘ ┴ └┘ └┘
src └────┘└───┘┴ ┴ └─┘ └┘
typ └────┘└───┘┴┴┴ └┘└─┘└┘└┘
doc └────┘ ┴ ┴ └─┘ └┘
txt └────┘ ┴ ┴ └─┘ └┘
par └────┘ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ └─┘ ┴┴
st ─────┘└──────────────────────┘└┘└
114 { intro e, injection e with e, subst b,
id ┴ ┴
src └─────┘ └────────┘ └─────┘ └────┘
typ └─────┘ └────────┘┴└─────┘ └────┘┴
doc └─────┘ └────────┘ └─────┘ └────┘
txt └─────┘ └────────┘ └─────┘ └────┘
par └─────┘ └────────┘ └─────┘ └────┘
pid └┘ ┴ └─────┘ ┴
st ────────────┘└──────────────────┘└───────┘└─
115 exact irrefl _ h } },
id └────┘ ┴
src └────┘└────┘└─┘ ┴
typ └────┘└────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────┘└──┘└
116 { intro a,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
117 have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
id ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴
src └─────┘┴└──┘ └─┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └─┘ ┴
typ └─────┘┴└──┘┴└─┘ ┴┴┴ ┴┴└────────────┘ ┴ ┴└┘└┘└┘└┘└───┘└┘┴┴└──┘ └┘ └─┘ ┴
doc └─────┘ └──┘ └─┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └─┘ ┴
txt └─────┘ └──┘ └─┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └─┘ ┴
par └─────┘ └──┘ └─┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └─┘ ┴
pid └───┘└┘ └──┘ └─┘ ┴ ┴ ┴ └───────┘└───┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └┘ └─┘ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
118 let b := (is_well_order.wf s).min _ this,
id └──────────────┘ ┴ └──┘
src └───────┘ └──────────────┘┴ └──────┘
typ └───────┘ └──────────────┘┴┴└──────┘└──┘
doc └───────┘ ┴ └──────┘
txt └───────┘ ┴ └──────┘
par └───────┘ ┴ └──────┘
pid └───┘┴└─┘ ┴ └──────┘
st ───────────────────────────────────────────┘└─
119 have ba : ¬r b a := (is_well_order.wf s).min_mem _ this,
id ┴ ┴ ┴ └──────────────┘ ┴ └──┘
src └────────┘ ┴ ┴ └──┘ └──────────────┘┴ └──────────┘
typ └────────┘ ┴┴┴┴┴└──┘ └──────────────┘┴┴└──────────┘└──┘
doc └────────┘ ┴ ┴ └──┘ ┴ └──────────┘
txt └────────┘ ┴ ┴ └──┘ ┴ └──────────┘
par └────────┘ ┴ ┴ └──┘ ┴ └──────────┘
pid └─────┘└─┘ ┴ ┴ └──┘ ┴ └──────────┘
st ──────────────────────────────────────────────────────────┘└─
120 refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
id ┴ └─────────┘ └┘
src └─────┘ └┘ └──┘ └──┘└─────────┘└─┘ ┴ └──────┘ ┴
typ └─────┘ └┘ ┴└──┘ └──┘└─────────┘└─┘ ┴ └──────┘└┘┴
doc └─────┘ └┘ └──┘ └──┘ └─┘ ┴ └──────┘ ┴
txt └─────┘ └┘ └──┘ └──┘ └─┘ ┴ └──────┘ ┴
par └─────┘ └┘ └──┘ └──┘ └─┘ ┴ └──────┘ ┴
pid ┴ └┘ └──┘ └──┘ └─┘ ┴ └──────┘ ┴
st ─────────────────────────────────────────────────────┘└─
121 rw [show ∀b:S, (⟨b, b.2⟩:S) = b, by intro b; cases b; refl],
id ┴ ┴ ┴
src └──┘ ┴ └┘ ┴ └┘ └──┘ └┘┴┴ └───┘└─────┘└┘└────┘ └┘└──┘┴
typ └──┘ ┴ └┘ ┴ └┘ └──┘┴└┘┴┴ └───┘└─────┘└┘└────┘┴└┘└──┘┴
doc └──┘ ┴ └┘ ┴ └┘ └──┘ └┘ ┴ └───┘└─────┘└┘└────┘ └┘└──┘┴
txt └──┘ ┴ └┘ ┴ └┘ └──┘ └┘ ┴ └───┘└─────┘└┘└────┘ └┘└──┘┴
par └──┘ ┴ └┘ ┴ └┘ └──┘ └┘ ┴ └───┘└─────┘└┘└────┘ └┘└──┘┴
pid └┘ ┴ └┘ ┴ └┘ └──┘ └┘ ┴ └──────────────────┘ └─────┘
st ──────────────────────────────────────┘└─────────────────────┘└──
122 exact (is_well_order.wf s).not_lt_min _ this
id └──────────────┘ ┴ └──┘
src └────┘ └──────────────┘┴ └─────────────┘ └
typ └────┘ └──────────────┘┴┴└─────────────┘└──┘└
doc └────┘ ┴ └─────────────┘ └
txt └────┘ ┴ └─────────────┘ └
par └────┘ ┴ └─────────────┘ └
pid ┴ ┴ └─────────────┘ └
st ─────────────────────────────────────────────────
123 (is_order_connected.neg_trans h ba) }
id └──────────────────────────┘ ┴ └┘
src ─────┘ └──────────────────────────┘┴ ┴ └┘
typ ─────┘ └──────────────────────────┘┴┴┴└┘└┘
doc ─────┘ ┴ ┴ └┘
txt ─────┘ ┴ ┴ └┘
par ─────┘ ┴ ┴ └┘
pid ─────┘ ┴ ┴ ┴┴
st ─────────────────────────────────────────┘└─
124 end
st ──┘
125
126 theorem lift_cof (o) : (cof o).lift = cof o.lift :=
id └─┘ ┴ └──┘ ┴ └─┘ ┴└───┘
src └─┘ └──┘ ┴ └─┘ └───┘
typ └─┘ ┴ └──┘ ┴ └─┘ ┴└───┘
doc └─┘ └──┘ └─┘ └───┘
127 induction_on o $ begin introsI α r _,
id └──────────┘ ┴
src └──────────┘ └───────────┘
typ └──────────┘ ┴ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └────┘
st └─────────────────┘└─
128 cases lift_type r with _ e, rw e,
id └───────┘ ┴ ┴
src └────┘└───────┘┴ └───────┘ └─┘
typ └────┘└───────┘┴┴└───────┘ └─┘┴
doc └────┘ ┴ └───────┘ └─┘
txt └────┘ ┴ └───────┘ └─┘
par └────┘ ┴ └───────┘ └─┘
pid ┴ ┴ └───────┘ ┴
st ───────────────────────────┘└────┘└─
129 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
130 { refine le_cof_type.2 (λ S H, _),
id └─────────┘
src └─────┘└─────────┘└─┘ └──────┘
typ └─────┘└─────────┘└─┘ └──────┘
doc └─────┘ └─┘ └──────┘
txt └─────┘ └─┘ └──────┘
par └─────┘ └─┘ └──────┘
pid ┴ └─┘ └──────┘
st ───┘└─────────────────────────────┘└─
131 have : (mk (ulift.up ⁻¹' S)).lift ≤ mk S :=
id └──────┘ └─┘ ┴ └┘ ┴
src └─────┘ ┴ └──────┘┴└─┘┴ └──────┘┴┴└┘┴ └───
typ └─────┘ ┴ └──────┘┴└─┘┴ └──────┘┴┴└┘┴┴└───
doc └─────┘ ┴ ┴└─┘┴ └──────┘ ┴└┘┴ └───
txt └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └───
st ────────────────────────────────────────────────
132 ⟨⟨λ ⟨⟨x, h⟩⟩, ⟨⟨x⟩, h⟩,
id ┴ ┴
src ────┘ └┘ └┘ └──┘ └─┘ └──
typ ────┘ └┘ ┴└┘┴└──┘ └─┘ └──
doc ────┘ └┘ └┘ └──┘ └─┘ └──
txt ────┘ └┘ └┘ └──┘ └─┘ └──
par ────┘ └┘ └┘ └──┘ └─┘ └──
pid ────┘ └┘ └┘ └──┘ └─┘ └──
st ─────────────────────────────
133 λ ⟨⟨x, h₁⟩⟩ ⟨⟨y, h₂⟩⟩ e, by simp at e; congr; injection e⟩⟩,
id ┴
src ──────┘ └┘ └┘ └──┘ └┘ └────┘ ┴└───────┘└┘└───┘└┘└────────┘ └┘
typ ──────┘ └┘ └┘ └──┘ └┘ └────┘ ┴└───────┘└┘└───┘└┘└────────┘┴└┘
doc ──────┘ └┘ └┘ └──┘ └┘ └────┘ ┴└───────┘└┘ └┘└────────┘ └┘
txt ──────┘ └┘ └┘ └──┘ └┘ └────┘ ┴└───────┘└┘└───┘└┘└────────┘ └┘
par ──────┘ └┘ └┘ └──┘ └┘ └────┘ ┴└───────┘└┘└───┘└┘└────────┘ └┘
pid ──────┘ └┘ └┘ └──┘ └┘ └────┘ └───────────────────────────┘ └┘
st ─────────────────────────────────┘└────────────────────────────┘└┘└─
134 refine le_trans (cardinal.lift_le.2 $ cof_type_le _ _) this,
id └──────┘ └──────────────┘ └─────────┘ └──┘
src └─────┘└──────┘┴ └──────────────┘└─┘ ┴└─────────┘└────┘
typ └─────┘└──────┘┴ └──────────────┘└─┘ ┴└─────────┘└────┘└──┘
doc └─────┘ ┴ └─┘ ┴ └────┘
txt └─────┘ ┴ └─┘ ┴ └────┘
par └─────┘ ┴ └─┘ ┴ └────┘
pid ┴ ┴ └─┘ ┴ └────┘
st ──────────────────────────────────────────────────────────────┘└─
135 exact λ a, let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩ in ⟨b, bs, br⟩ },
id ┴ └┘ └┘ ┴
src └────┘ └──┘ ┴ └─┘ └┘ └───┘ ┴ └───┘ └┘ └┘ └┘
typ └────┘ └──┘ ┴ ┴└─┘└┘└┘└┘└───┘┴┴ └───┘ └┘ └┘ └┘
doc └────┘ └──┘ ┴ └─┘ └┘ └───┘ ┴ └───┘ └┘ └┘ └┘
txt └────┘ └──┘ ┴ └─┘ └┘ └───┘ ┴ └───┘ └┘ └┘ └┘
par └────┘ └──┘ ┴ └─┘ └┘ └───┘ ┴ └───┘ └┘ └┘ └┘
pid ┴ └──┘ ┴ └─┘ └┘ └───┘ ┴ └───┘ └┘ └┘ ┴┴
st ────────────────────────────────────────────────────────┘└┘└
136 { rcases cof_eq r with ⟨S, H, e'⟩,
id └────┘ ┴
src └─────┘└────┘┴ └──────────────┘
typ └─────┘└────┘┴┴└──────────────┘
doc └─────┘ ┴ └──────────────┘
txt └─────┘ ┴ └──────────────┘
par └─────┘ ┴ └──────────────┘
pid ┴ ┴ └──────────────┘
st ──────────────────────────────────┘└─
137 have : mk (ulift.down ⁻¹' S) ≤ (mk S).lift :=
id └────────┘ └┘ ┴
src └─────┘ ┴ └────────┘┴ ┴ └┘ ┴ └┘┴ └─────────
typ └─────┘ ┴ └────────┘┴ ┴ └┘ ┴ └┘┴┴└─────────
doc └─────┘ ┴ ┴ ┴ └┘ ┴ └┘┴ └─────────
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────────
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────────
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘└────
st ──────────────────────────────────────────────────
138 ⟨⟨λ ⟨⟨x⟩, h⟩, ⟨⟨x, h⟩⟩,
id ┴ ┴
src ────┘ └┘ └─┘ └─┘ └┘ └───
typ ────┘ └┘ ┴└─┘┴└─┘ └┘ └───
doc ────┘ └┘ └─┘ └─┘ └┘ └───
txt ────┘ └┘ └─┘ └─┘ └┘ └───
par ────┘ └┘ └─┘ └─┘ └┘ └───
pid ────┘ └┘ └─┘ └─┘ └┘ └───
st ─────────────────────────────
139 λ ⟨⟨x⟩, h₁⟩ ⟨⟨y⟩, h₂⟩ e, by simp at e; congr; injections⟩⟩,
src ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ ┴└───────┘└┘└───┘└┘└────────┘└┘
typ ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ ┴└───────┘└┘└───┘└┘└────────┘└┘
doc ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ ┴└───────┘└┘ └┘└────────┘└┘
txt ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ ┴└───────┘└┘└───┘└┘└────────┘└┘
par ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ ┴└───────┘└┘└───┘└┘└────────┘└┘
pid ──────┘ └┘ └─┘ └─┘ └─┘ └───┘ └─────────────────────────────┘
st ─────────────────────────────────┘└───────────────────────────┘└┘└─
140 rw e' at this,
id └┘
src └─┘ └──────┘
typ └─┘└┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────┘└─
141 refine le_trans (cof_type_le _ _) this,
id └──────┘ └─────────┘ └──┘
src └─────┘└──────┘┴ └─────────┘└────┘
typ └─────┘└──────┘┴ └─────────┘└────┘└──┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ─────────────────────────────────────────┘└─
142 exact λ ⟨a⟩, let ⟨b, bs, br⟩ := H a in ⟨⟨b⟩, bs, br⟩ }
id ┴ ┴ └┘ └┘ ┴
src └────┘ └┘ └─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └┘ └┘
typ └────┘ └┘┴└─┘ ┴ ┴└┘└┘└┘└┘└───┘┴┴ └──┘ └─┘ └┘ └┘
doc └────┘ └┘ └─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └┘ └┘
txt └────┘ └┘ └─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └┘ └┘
par └────┘ └┘ └─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └┘ └┘
pid ┴ └┘ └─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └┘ ┴┴
st ────────────────────────────────────────────────────────┘└─
143 end
st ──┘
144
145 theorem cof_le_card (o) : cof o ≤ card o :=
id └─┘ ┴ ┴ └──┘ ┴
src └─┘ ┴ └──┘
typ └─┘ ┴ ┴ └──┘ ┴
doc └─┘ └──┘
146 induction_on o $ λ α r _, begin
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴
st └─────
147 resetI,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ──────────
148 have : mk (@set.univ α) = card (type r) :=
id └┘ └──────┘ ┴ ┴ └──┘ └──┘ ┴
src └─────┘└┘┴ └──────┘┴ └┘┴┴└──┘┴ └──┘┴ └────
typ └─────┘└┘┴ └──────┘┴┴└┘┴┴└──┘┴ └──┘┴┴└────
doc └─────┘└┘┴ ┴ └┘ ┴└──┘┴ └──┘┴ └────
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└───
st ─────────────────────────────────────────────
149 quotient.sound ⟨equiv.set.univ _⟩,
id └────────────┘ └────────────┘
src ───┘└────────────┘┴ └────────────┘└─┘
typ ───┘└────────────┘┴ └────────────┘└─┘
doc ───┘ ┴ └─┘
txt ───┘ ┴ └─┘
par ───┘ ┴ └─┘
pid ───┘ ┴ └─┘
st ────────────────────────────────────┘└─
150 rw ← this, exact cof_type_le set.univ (λ a, ⟨a, ⟨⟩, irrefl a⟩)
id └──┘ └─────────┘ └──────┘ ┴ └────┘
src └───┘ └────┘└─────────┘┴└──────┘┴ └──┘ └┘┴└─┘└────┘┴ └─┘
typ └───┘└──┘ └────┘└─────────┘┴└──────┘┴ └──┘ └┘┴└─┘└────┘┴ └─┘
doc └───┘ └────┘ ┴ ┴ └──┘ └┘ └─┘ ┴ └─┘
txt └───┘ └────┘ ┴ ┴ └──┘ └┘ └─┘ ┴ └─┘
par └───┘ └────┘ ┴ ┴ └──┘ └┘ └─┘ ┴ └─┘
pid └─┘ ┴ ┴ ┴ └──┘ └┘ └─┘ ┴ └┘┴
st ──────────┘└────────────────────────────────────────────────────┘
151 end
st └─┘
152
153 theorem cof_ord_le (c : cardinal) : cof c.ord ≤ c :=
id └──────┘ └─┘ ┴└──┘ ┴ ┴
src └──────┘ └─┘ └──┘ ┴
typ └──────┘ └─┘ ┴└──┘ ┴ ┴
doc └──────┘ └─┘ └──┘
154 by simpa using cof_le_card c.ord
id └─────────┘ └───┘
src └──────────┘└─────────┘┴└───┘└
typ └──────────┘└─────────┘┴└───┘└
doc └──────────┘ ┴└───┘└
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st └──────────────────────────────
155
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
156 @[simp] theorem cof_zero : cof 0 = 0 :=
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
doc └──┘ └─┘
157 le_antisymm (by simpa using cof_le_card 0) (cardinal.zero_le _)
id └─────────┘ └─────────┘ └──────────────┘
src └─────────┘ └──────────┘└─────────┘└┘ └──────────────┘
typ └─────────┘ └──────────┘└─────────┘└┘ └──────────────┘
doc └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid ┴└────┘ ┴┴
st └────────────────────────┘
158
159 @[simp] theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
160 ⟨induction_on o $ λ α r _ z, by exactI
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └──────
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──────
doc └──────
txt └──────
par └──────
pid └
st └───────
161 let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_empty.2 $
id └┘ ┴ └────┘ ┴ └────────────────────┘
src ─┘ ┴ └┘ └┘ └───┘└────┘┴ └──┘└────────────────────┘└─┘ └
typ ─┘ ┴ └┘└┘└┘┴└───┘└────┘┴┴└──┘└────────────────────┘└─┘ └
doc ─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └
txt ─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └
par ─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └
pid ─┘ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ └
st ───────────────────────────────────────────────────────────
162 λ ⟨a⟩, let ⟨b, h, _⟩ := hl a in
id ┴
src ─┘ └┘ └─┘ ┴ └┘ └──────┘ ┴ └───
typ ─┘ └┘┴└─┘ ┴ └┘ └──────┘ ┴ └───
doc ─┘ └┘ └─┘ ┴ └┘ └──────┘ ┴ └───
txt ─┘ └┘ └─┘ ┴ └┘ └──────┘ ┴ └───
par ─┘ └┘ └─┘ ┴ └┘ └──────┘ ┴ └───
pid ─┘ └┘ └─┘ ┴ └┘ └──────┘ ┴ └───
st ──────────────────────────────────
163 ne_zero_iff_nonempty.2 (by exact ⟨⟨_, h⟩⟩) (e.trans z),
id └──────────────────┘ ┴ └────┘ ┴
src ─┘└──────────────────┘└─┘ ┴└────┘ └─┘ └┘└┘ └────┘┴ ┴
typ ─┘└──────────────────┘└─┘ └─────┘ └─┘┴└──┘ └────┘┴┴┴
doc ─┘ └─┘ ┴└────┘ └─┘ └┘└┘ ┴ ┴
txt ─┘ └─┘ ┴└────┘ └─┘ └┘└┘ ┴ ┴
par ─┘ └─┘ └─────┘ └─┘ └──┘ ┴ ┴
pid ─┘ └─┘ └─────┘ └─┘ └──┘ ┴ ┴
st ───────────────────────────┘└─────────────┘└───────────┘
164 λ e, by simp [e]⟩
id ┴ ┴
src └────┘ ┴
typ ┴ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
165
166 @[simp] theorem cof_succ (o) : cof (succ o) = 1 :=
id └─┘ └──┘ ┴ ┴
src └─┘ └──┘ ┴
typ └─┘ └──┘ ┴ ┴
doc └──┘ └─┘ └──┘
167 begin
st └─────
168 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
169 { refine induction_on o (λ α r _, _),
id └──────────┘ ┴
src └─────┘└──────────┘┴ ┴ └────────┘
typ └─────┘└──────────┘┴┴┴ └────────┘
doc └─────┘ ┴ ┴ └────────┘
txt └─────┘ ┴ ┴ └────────┘
par └─────┘ ┴ ┴ └────────┘
pid ┴ ┴ ┴ └────────┘
st ───┘└────────────────────────────────┘└─
170 change cof (type _) ≤ _,
id └─┘ └──┘ ┴
src └─────┘└─┘┴ └──┘└──┘┴└┘
typ └─────┘└─┘┴ └──┘└──┘┴└┘
doc └─────┘└─┘┴ └──┘└──┘ └┘
txt └─────┘ ┴ └──┘ └┘
par └─────┘ ┴ └──┘ └┘
pid ┴ ┴ └──┘ └┘
st ──────────────────────────┘└─
171 rw [← (_ : mk _ = 1)], apply cof_type_le,
id └┘ ┴ └─────────┘
src └────┘ └──┘└┘└─┘┴└──┘ └────┘└─────────┘
typ └────┘ └──┘└┘└─┘┴└──┘ └────┘└─────────┘
doc └────┘ └──┘└┘└─┘ └──┘ └────┘
txt └────┘ └──┘ └─┘ └──┘ └────┘
par └────┘ └──┘ └─┘ └──┘ └────┘
pid └──┘ └──┘ └─┘ └──┘ ┴
st ───────────────────────┘└──────────────────┘└─
172 { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
id └─────┘ └────────┘ └───────────────┘
src └─────┘ └──┘ └─────┘┴└────────┘└┘└───────────────┘└────┘
typ └─────┘ └──┘ └─────┘┴└────────┘└┘└───────────────┘└────┘
doc └─────┘ └──┘ ┴ └┘ └────┘
txt └─────┘ └──┘ ┴ └┘ └────┘
par └─────┘ └──┘ ┴ └┘ └────┘
pid ┴ └──┘ ┴ └┘ └────┘
st ─────┘└──────────────────────────────────────────────────────┘└─
173 rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
id ┴ └────────────┘
src └─────┘ └────────────┘ └────┘└────────────┘└┘
typ └─────┘┴└────────────┘ └────┘└────────────┘└┘
doc └─────┘ └────────────┘ └────┘ └┘
txt └─────┘ └────────────┘ └────┘ └┘
par └─────┘ └────────────┘ └────┘ └┘
pid ┴ └────────────┘ ┴┴ ┴┴
st ───────────────────────────────────────────────────┘└┘└
174 { rw [cardinal.fintype_card, set.card_singleton], simp } },
id └───────────────────┘ └────────────────┘
src └──┘└───────────────────┘└┘└────────────────┘┴ └───┘
typ └──┘└───────────────────┘└┘└────────────────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st ──────────────────────────────┘└──────────────────┘└──────┘└──┘└
175 { rw [← cardinal.succ_zero, cardinal.succ_le],
id └────────────────┘ └──────────────┘
src └────┘└────────────────┘└┘└──────────────┘┴
typ └────┘└────────────────┘└┘└──────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ───────────────────────────┘└────────────────┘└──
176 simpa [lt_iff_le_and_ne, cardinal.zero_le] using
id └──────────────┘ └──────────────┘
src └─────┘└──────────────┘└┘└──────────────┘└───────
typ └─────┘└──────────────┘└┘└──────────────┘└───────
doc └─────┘ └┘ └───────
txt └─────┘ └┘ └───────
par └─────┘ └┘ └───────
pid ┴┴ └┘ ┴┴└─────
st ─────────────────────────────────────────────────────
177 λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
id └──────────┘ ┴ └─────────┘ └─────┘
src ─────┘ └──┘└──────────┘┴ ┴ └─────────┘└─┘ └─────┘┴ └─┘
typ ─────┘ └──┘└──────────┘┴┴┴ └─────────┘└─┘ └─────┘┴ └─┘
doc ─────┘ └──┘ ┴ ┴ └─┘ ┴ └─┘
txt ─────┘ └──┘ ┴ ┴ └─┘ ┴ └─┘
par ─────┘ └──┘ ┴ ┴ └─┘ ┴ └─┘
pid ─────┘ └──┘ ┴ ┴ └─┘ ┴ └┘┴
st ─────────────────────────────────────────────────────┘└─
178 end
st ──┘
179
180 @[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
id └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘ ┴
doc └──┘ └─┘ └──┘
181 ⟨induction_on o $ λ α r _ z, begin
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
st └─────
182 resetI,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ──────────
183 rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
id └────┘ ┴ ┴
src └─────┘└────┘┴ └──────────────┘ └─┘ └───┘
typ └─────┘└────┘┴┴└──────────────┘ └─┘┴└───┘
doc └─────┘ ┴ └──────────────┘ └─┘ └───┘
txt └─────┘ ┴ └──────────────┘ └─┘ └───┘
par └─────┘ ┴ └──────────────┘ └─┘ └───┘
pid ┴ ┴ └──────────────┘ ┴ └───┘
st ────────────────────────────────┘└─────────┘└─
184 cases ne_zero_iff_nonempty.1 (by rw e; exact one_ne_zero) with a,
id └──────────────────┘ ┴ └─────────┘
src └────┘└──────────────────┘└─┘ ┴└─┘ └┘└────┘└─────────┘└──────┘
typ └────┘└──────────────────┘└─┘ ┴└─┘┴└┘└────┘└─────────┘└──────┘
doc └────┘ └─┘ ┴└─┘ └┘└────┘ └──────┘
txt └────┘ └─┘ ┴└─┘ └┘└────┘ └──────┘
par └────┘ └─┘ ┴└─┘ └┘└────┘ └──────┘
pid ┴ └─┘ └──┘ └──────┘ ┴└─────┘
st ─────────────────────────────────┘└──────────────────────┘└──────┘└─
185 refine ⟨typein r a, eq.symm $ quotient.sound
id └────┘ ┴ ┴ └─────┘ └────────────┘
src └─────┘ └────┘┴ ┴ └┘└─────┘┴ ┴└────────────┘└
typ └─────┘ └────┘┴┴┴┴└┘└─────┘┴ ┴└────────────┘└
doc └─────┘ └────┘┴ ┴ └┘ ┴ ┴ └
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └
par └─────┘ ┴ ┴ └┘ ┴ ┴ └
pid ┴ ┴ ┴ └┘ ┴ ┴ └
st ───────────────────────────────────────────────
186 ⟨order_iso.of_surjective (order_embedding.of_monotone _
id └─────────────────────┘ └─────────────────────────┘
src ───┘ └─────────────────────┘┴ └─────────────────────────┘└──
typ ───┘ └─────────────────────┘┴ └─────────────────────────┘└──
doc ───┘ ┴ └─────────────────────────┘└──
txt ───┘ ┴ └──
par ───┘ ┴ └──
pid ───┘ ┴ └──
st ────────────────────────────────────────────────────────────
187 (λ x y, _)) (λ x, _)⟩⟩,
src ─────┘ └────────┘ └──────┘
typ ─────┘ └────────┘ └──────┘
doc ─────┘ └────────┘ └──────┘
txt ─────┘ └────────┘ └──────┘
par ─────┘ └────────┘ └──────┘
pid ─────┘ └────────┘ └──────┘
st ───────────────────────────┘└─
188 { apply sum.rec; [exact subtype.val, exact λ _, a] },
id └─────┘ ┴ └─────────┘ ┴
src └────┘└─────┘ ┴└────┘└─────────┘ └────┘ └──┘
typ └────┘└─────┘ ┴└────┘└─────────┘ └────┘ └──┘┴
doc └────┘ └────┘ └────┘ └──┘
txt └────┘ └────┘ └────┘ └──┘
par └────┘ └────┘ └────┘ └──┘
pid ┴ ┴ ┴ └──┘
st ───┘└──────────────────────────────────────────────┘└─┘└
189 { rcases x with x|⟨⟨⟨⟩⟩⟩; rcases y with y|⟨⟨⟨⟩⟩⟩;
id ┴ ┴
src └─────┘ └────────────┘ └─────┘ └────────────┘
typ └─────┘┴└────────────┘ └─────┘┴└────────────┘
doc └─────┘ └────────────┘ └─────┘ └────────────┘
txt └─────┘ └────────────┘ └─────┘ └────────────┘
par └─────┘ └────────────┘ └─────┘ └────────────┘
pid ┴ └────────────┘ ┴ └────────────┘
st ───┘└───────────────────────────────────────────────
190 simp [subrel, order.preimage, empty_relation],
id └────┘ └────────────┘ └────────────┘
src └────┘└────┘└┘└────────────┘└┘└────────────┘┴
typ └────┘└────┘└┘└────────────┘└┘└────────────┘┴
doc └────┘└────┘└┘└────────────┘└┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ──────────────────────────────────────────────────┘└─
191 exact x.2 },
id ┴
src └────┘ └─┘
typ └────┘┴└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────┘└┘└
192 { suffices : r x a ∨ ∃ (b : punit), ↑a = x, {simpa},
id ┴ ┴ └───┘ ┴ ┴┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ ┴┴└────┘└───┘┴┴┴┴ ┴┴┴ └───┘
typ └─────────┘┴┴ ┴ ┴ ┴┴└────┘└───┘┴┴┴┴┴┴┴┴┴ └───┘
doc └─────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───┘
txt └─────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───┘
par └─────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───┘
pid └───────┘└┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘└──────┘└┘└
193 rcases trichotomous_of r x a with h|h|h,
id └─────────────┘ ┴ ┴ ┴
src └─────┘└─────────────┘┴ ┴ ┴ └─────────┘
typ └─────┘└─────────────┘┴┴┴┴┴┴└─────────┘
doc └─────┘ ┴ ┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ ┴ └─────────┘
st ──────────────────────────────────────────┘└─
194 { exact or.inl h },
id └────┘ ┴
src └────┘└────┘┴ ┴
typ └────┘└────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└─────────────┘└┘└
195 { exact or.inr ⟨punit.star, h.symm⟩ },
id └────┘ └────────┘ └────┘
src └────┘└────┘┴ └────────┘└┘└────┘└┘
typ └────┘└────┘┴ └────────┘└┘└────┘└┘
doc └────┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘
pid ┴ ┴ └┘ ┴┴
st ─────┘└────────────────────────────────┘└┘└
196 { rcases hl x with ⟨a', aS, hn⟩,
id └┘ ┴
src └─────┘ ┴ └────────────────┘
typ └─────┘└┘┴┴└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ──────────────────────────────────┘└─
197 rw (_ : ↑a = a') at h, {exact absurd h hn},
id ┴ └┘ └────┘ ┴ └┘
src └─┘ └──┘ ┴ ┴ └────┘ └────┘└────┘┴ ┴
typ └─┘ └──┘ ┴┴ ┴└┘└────┘ └────┘└────┘┴┴┴└┘
doc └─┘ └──┘ ┴ ┴ └────┘ └────┘ ┴ ┴
txt └─┘ └──┘ ┴ ┴ └────┘ └────┘ ┴ ┴
par └─┘ └──┘ ┴ ┴ └────┘ └────┘ ┴ ┴
pid ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴
st ──────────────────────────┘└──────────────────┘└┘└
198 refine congr_arg subtype.val (_ : a = ⟨a', aS⟩),
id └───────┘ └─────────┘ ┴ └┘ └┘
src └─────┘└───────┘┴└─────────┘┴ └──┘ ┴ ┴ └┘ └┘
typ └─────┘└───────┘┴└─────────┘┴ └──┘┴┴ ┴ └┘└┘└┘└┘
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ └┘ └┘
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ └┘ └┘
par └─────┘ ┴ ┴ └──┘ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └┘
st ────────────────────────────────────────────────────┘└─
199 haveI := le_one_iff_subsingleton.1 (le_of_eq e),
id └─────────────────────┘ └──────┘ ┴
src └───────┘└─────────────────────┘└─┘ └──────┘┴ ┴
typ └───────┘└─────────────────────┘└─┘ └──────┘┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴└─┘ └─┘ ┴ ┴
st ────────────────────────────────────────────────────┘└─
200 apply subsingleton.elim } }
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└───
201 end, λ ⟨a, e⟩, by simp [e]⟩
id ┴ ┴
src └────┘ ┴
typ ┴ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──┘ └───────┘
202
203 @[simp] theorem cof_add (a b : ordinal) : b ≠ 0 → cof (a + b) = cof b :=
id └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘ ┴ ┴ └─┘
typ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └─────┘ └─┘ └─┘
204 induction_on a $ λ α r _, induction_on b $ λ β s _ b0, begin
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
st └─────
205 resetI,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ──────────
206 change cof (type _) = _,
id └─┘ └──┘ ┴
src └─────┘└─┘┴ └──┘└──┘┴└┘
typ └─────┘└─┘┴ └──┘└──┘┴└┘
doc └─────┘└─┘┴ └──┘└──┘ └┘
txt └─────┘ ┴ └──┘ └┘
par └─────┘ ┴ └──┘ └┘
pid ┴ ┴ └──┘ └┘
st ────────────────────────┘└─
207 refine eq_of_forall_le_iff (λ c, _),
id └─────────────────┘
src └─────┘└─────────────────┘┴ └────┘
typ └─────┘└─────────────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ────────────────────────────────────┘└─
208 rw [le_cof_type, le_cof_type],
id └─────────┘ └─────────┘
src └──┘└─────────┘└┘└─────────┘┴
typ └──┘└─────────┘└┘└─────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────┘└───────────┘└──
209 split; intros H S hS,
src └───┘ └───────────┘
typ └───┘ └───────────┘
doc └───┘ └───────────┘
txt └───┘ └───────────┘
par └───┘ └───────────┘
pid └─────┘
st ─────────────────────┘└─
210 { refine le_trans (H {a | sum.rec_on a (∅:set α) S} (λ a, _)) ⟨⟨_, _⟩⟩,
id └──────┘ ┴ ┴ └────────┘ ┴ └─┘ ┴ ┴
src └─────┘└──────┘┴ ┴┴└──┘└────────┘┴ ┴ ┴┴└─┘┴ └┘ └┘ └──────┘ └────┘
typ └─────┘└──────┘┴ ┴┴┴└──┘└────────┘┴ ┴ ┴┴└─┘┴┴└┘┴└┘ └──────┘ └────┘
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘ └────┘
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘ └────┘
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘ └────┘
pid ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────┘ └────┘
st ───┘└──────────────────────────────────────────────────────────────────┘└─
211 { cases a with a b,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ─────┘└──────────────┘└─
212 { cases type_ne_zero_iff_nonempty.1 b0 with b,
id └───────────────────────┘ └┘
src └────┘└───────────────────────┘└─┘ └─────┘
typ └────┘└───────────────────────┘└─┘└┘└─────┘
doc └────┘ └─┘ └─────┘
txt └────┘ └─┘ └─────┘
par └────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────┘└─────────────────────────────────────────┘└─
213 rcases hS b with ⟨b', bs, _⟩,
id └┘ ┴
src └─────┘ ┴ └───────────────┘
typ └─────┘└┘┴┴└───────────────┘
doc └─────┘ ┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ───────────────────────────────────┘└─
214 exact ⟨sum.inr b', bs, by simp⟩ },
id └─────┘ └┘ └┘
src └────┘ └─────┘┴ └┘ └┘ ┴└──┘└┘
typ └────┘ └─────┘┴└┘└┘└┘└┘ ┴└──┘└┘
doc └────┘ ┴ └┘ └┘ ┴└──┘└┘
txt └────┘ ┴ └┘ └┘ ┴└──┘└┘
par └────┘ ┴ └┘ └┘ ┴└──┘└┘
pid ┴ ┴ └┘ └┘ └────┘┴
st ────────────────────────────────┘└───┘└┘└┘└
215 { rcases hS b with ⟨b', bs, h⟩,
id └┘ ┴
src └─────┘ ┴ └───────────────┘
typ └─────┘└┘┴┴└───────────────┘
doc └─────┘ ┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ───────────────────────────────────┘└─
216 exact ⟨sum.inr b', bs, by simp [h]⟩ } },
id └─────┘ └┘ └┘ ┴
src └────┘ └─────┘┴ └┘ └┘ ┴└────┘ ┴└┘
typ └────┘ └─────┘┴└┘└┘└┘└┘ ┴└────┘┴┴└┘
doc └────┘ ┴ └┘ └┘ ┴└────┘ ┴└┘
txt └────┘ ┴ └┘ └┘ ┴└────┘ ┴└┘
par └────┘ ┴ └┘ └┘ ┴└────┘ ┴└┘
pid ┴ ┴ └┘ └┘ └─────┘ └┘┴
st ────────────────────────────────┘└───────┘└┘└──┘└
217 { exact λ a, match a with ⟨sum.inr b, h⟩ := ⟨b, h⟩ end },
id ┴ ┴
src └────┘ └──┘ ┴ └────┘ ┴ └┘ └───┘ └┘ └────┘
typ └────┘ └──┘ ┴ └────┘ ┴┴└┘┴└───┘ └┘ └────┘
doc └────┘ └──┘ ┴ └────┘ ┴ └┘ └───┘ └┘ └────┘
txt └────┘ └──┘ ┴ └────┘ ┴ └┘ └───┘ └┘ └────┘
par └────┘ └──┘ ┴ └────┘ ┴ └┘ └───┘ └┘ └────┘
pid ┴ └──┘ ┴ └────┘ ┴ └┘ └───┘ └┘ └───┘┴
st ─────┘└───────────────────────────────────────────────────┘└┘└
218 { exact λ a b, match a, b with
src └────┘ └────┘ ┴ └┘ └─────
typ └────┘ └────┘ ┴ └┘ └─────
doc └────┘ └────┘ ┴ └┘ └─────
txt └────┘ └────┘ ┴ └┘ └─────
par └────┘ └────┘ ┴ └┘ └─────
pid ┴ └────┘ ┴ └┘ └─────
st ───────────────────────────────────
219 ⟨sum.inr a, h₁⟩, ⟨sum.inr b, h₂⟩, h := by congr; injection h
id ┴
src ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ ┴└───┘└┘└────────┘ └
typ ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ ┴└───┘└┘└────────┘┴└
doc ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ ┴ └┘└────────┘ └
txt ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ ┴└───┘└┘└────────┘ └
par ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ ┴└───┘└┘└────────┘ └
pid ───────┘ ┴ └┘ └─┘ ┴ └┘ └─┘ └──┘ └────────────────┘ └
st ────────────────────────────────────────────────┘└───────────────────
220 end } },
src ─────┘└──┘
typ ─────┘└──┘
doc ─────┘└──┘
txt ─────┘└──┘
par ─────┘└──┘
pid ────────┘┴
st ─────┘└──┘└──┘└
221 { refine le_trans (H (sum.inr ⁻¹' S) (λ a, _)) ⟨⟨_, _⟩⟩,
id └──────┘ ┴ └─────┘ └─┘ ┴
src └─────┘└──────┘┴ ┴ └─────┘┴└─┘┴ └┘ └──────┘ └────┘
typ └─────┘└──────┘┴ ┴┴ └─────┘┴└─┘┴┴└┘ └──────┘ └────┘
doc └─────┘ ┴ ┴ ┴└─┘┴ └┘ └──────┘ └────┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ └──────┘ └────┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ └──────┘ └────┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └──────┘ └────┘
st ────────────────────────────────────────────────────────┘└─
222 { rcases hS (sum.inr a) with ⟨a'|b', bs, h⟩; simp at h,
id └┘ └─────┘ ┴
src └─────┘ ┴ └─────┘┴ └───────────────────┘ └───────┘
typ └─────┘└┘┴ └─────┘┴┴└───────────────────┘ └───────┘
doc └─────┘ ┴ ┴ └───────────────────┘ └───────┘
txt └─────┘ ┴ ┴ └───────────────────┘ └───────┘
par └─────┘ ┴ ┴ └───────────────────┘ └───────┘
pid ┴ ┴ ┴ └───────────────────┘ ┴└──┘
st ─────┘└──────────────────────────────────────────────────┘└─
223 { cases h }, { exact ⟨b', bs, h⟩ } },
id ┴ └┘ └┘ ┴
src └────┘ ┴ └────┘ └┘ └┘ └┘
typ └────┘┴┴ └────┘ └┘└┘└┘└┘┴└┘
doc └────┘ ┴ └────┘ └┘ └┘ └┘
txt └────┘ ┴ └────┘ └┘ └┘ └┘
par └────┘ ┴ └────┘ └┘ └┘ └┘
pid ┴ ┴ ┴ └┘ └┘ ┴┴
st ───────┘└──────┘└┘└───────────────────┘└──┘└
224 { exact λ ⟨a, h⟩, ⟨_, h⟩ },
id ┴
src └────┘ └┘ └┘ └─┘ └─┘ └┘
typ └────┘ └┘ └┘┴└─┘ └─┘ └┘
doc └────┘ └┘ └┘ └─┘ └─┘ └┘
txt └────┘ └┘ └┘ └─┘ └─┘ └┘
par └────┘ └┘ └┘ └─┘ └─┘ └┘
pid ┴ └┘ └┘ └─┘ └─┘ ┴┴
st ─────┘└─────────────────────┘└┘└
225 { exact λ ⟨a, h₁⟩ ⟨b, h₂⟩ h,
src └────┘ └┘ └┘ └─┘ └┘ └────
typ └────┘ └┘ └┘ └─┘ └┘ └────
doc └────┘ └┘ └┘ └─┘ └┘ └────
txt └────┘ └┘ └┘ └─┘ └┘ └────
par └────┘ └┘ └┘ └─┘ └┘ └────
pid ┴ └┘ └┘ └─┘ └┘ └────
st ─────────────────────────────────
226 by injection h with h; congr; injection h } }
id ┴ ┴
src ───────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴
typ ───────┘ ┴└────────┘┴└─────┘└┘└───┘└┘└────────┘┴┴
doc ───────┘ ┴└────────┘ └─────┘└┘ └┘└────────┘ ┴
txt ───────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴
par ───────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴
pid ───────┘ └─────────┘ └────────────────────────┘ ┴
st ─────────┘└──────────────────────────────────────┘└───
227 end
st ──┘
228
229 @[simp] theorem cof_cof (o : ordinal) : cof (cof o).ord = cof o :=
id └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └─┘ ┴
src └─────┘ └─┘ └─┘ └─┘ ┴ └─┘
typ └─────┘ └─┘ └─┘ ┴ └─┘ ┴ └─┘ ┴
doc └──┘ └─────┘ └─┘ └─┘ └─┘ └─┘
230 le_antisymm (le_trans (cof_le_card _) (by simp)) $
id └─────────┘ └──────┘ └─────────┘
src └─────────┘ └──────┘ └─────────┘ └──┘
typ └─────────┘ └──────┘ └─────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
231 induction_on o $ λ α r _, by exactI
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └─────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st └───────
232 let ⟨S, hS, e₁⟩ := ord_cof_eq r,
id ┴ └────────┘ ┴
src ┴ └┘ └┘ └───┘└────────┘┴ └─
typ ┴ ┴└┘ └┘ └───┘└────────┘┴┴└─
doc ┴ └┘ └┘ └───┘ ┴ └─
txt ┴ └┘ └┘ └───┘ ┴ └─
par ┴ └┘ └┘ └───┘ ┴ └─
pid ┴ └┘ └┘ └───┘ ┴ └─
st ─────────────────────────────────
233 ⟨T, hT, e₂⟩ := cof_eq (subrel r S) in begin
id └────┘ └────┘
src ───┘ └┘ └┘ └───┘└────┘┴ └────┘┴ ┴ └───┘ └
typ ───┘ └┘ └┘ └───┘└────┘┴ └────┘┴ ┴ └───┘ └
doc ───┘ └┘ └┘ └───┘ ┴ └────┘┴ ┴ └───┘ └
txt ───┘ └┘ └┘ └───┘ ┴ ┴ ┴ └───┘ └
par ───┘ └┘ └┘ └───┘ ┴ ┴ ┴ └───┘ └
pid ───┘ └┘ └┘ └───┘ ┴ ┴ ┴ └───┘ └
st ─────────────────────────────────────────┘└─────
234 rw e₁ at e₂, rw ← e₂,
id └┘ └┘
src ─┘└─┘ └────┘└┘└───┘ └─
typ ─┘└─┘└┘└────┘└┘└───┘└┘└─
doc ─┘└─┘ └────┘└┘└───┘ └─
txt ─┘└─┘ └────┘└┘└───┘ └─
par ─┘└─┘ └────┘└┘└───┘ └─
pid ────┘ └───────────┘ └─
st ────────────┘└───────┘└─
235 refine le_trans (cof_type_le {a | ∃ h, (subtype.mk a h : S) ∈ T} (λ a, _)) ⟨⟨_, _⟩⟩,
id └──────┘ └─────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src ─┘└─────┘└──────┘┴ └─────────┘┴┴└──┘┴└┘┴┴ └────────┘┴ ┴ └─┘ └┘┴┴ └┘ └──────┘ └────┘└─
typ ────────┘└──────┘┴ └─────────┘┴┴└──┘┴└┘┴┴ └────────┘┴ ┴ └─┘┴└┘┴┴┴└┘ └──────┘ └───────
doc ─┘└─────┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └──────┘ └────┘└─
txt ─┘└─────┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └──────┘ └────┘└─
par ────────┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └──────┘ └───────
pid ────────┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └──────┘ └───────
st ────────────────────────────────────────────────────────────────────────────────────┘└─
236 { rcases hS a with ⟨b, bS, br⟩,
id └┘ ┴
src ───┘└─────┘ ┴ └───────────────┘└─
typ ───┘└─────┘└┘┴┴└───────────────┘└─
doc ───┘└─────┘ ┴ └───────────────┘└─
txt ───┘└─────┘ ┴ └───────────────┘└─
par ───┘└─────┘ ┴ └───────────────┘└─
pid ──────────┘ ┴ └──────────────────
st ──┘└───────────────────────────┘└─
237 rcases hT ⟨b, bS⟩ with ⟨⟨c, cS⟩, cT, cs⟩,
id └┘ ┴ └┘
src ───┘└─────┘ ┴ └┘ └──────────────────────┘└─
typ ───┘└─────┘└┘┴ ┴└┘└┘└──────────────────────┘└─
doc ───┘└─────┘ ┴ └┘ └──────────────────────┘└─
txt ───┘└─────┘ ┴ └┘ └──────────────────────┘└─
par ───┘└─────┘ ┴ └┘ └──────────────────────┘└─
pid ──────────┘ ┴ └┘ └─────────────────────────
st ───────────────────────────────────────────┘└─
238 exact ⟨c, ⟨cS, cT⟩, is_order_connected.neg_trans cs br⟩ },
id ┴ └┘ └┘ └──────────────────────────┘ └┘ └┘
src ───┘└────┘ └┘ └┘ └─┘└──────────────────────────┘┴ ┴ └┘└──
typ ─────────┘ ┴└┘ └┘└┘└┘└─┘└──────────────────────────┘┴└┘┴└┘└────
doc ───┘└────┘ └┘ └┘ └─┘ ┴ ┴ └┘└──
txt ───┘└────┘ └┘ └┘ └─┘ ┴ ┴ └┘└──
par ─────────┘ └┘ └┘ └─┘ ┴ ┴ └────
pid ─────────┘ └┘ └┘ └─┘ ┴ ┴ └────
st ───────────────────────────────────────────────────────────┘┴└─
239 { exact λ ⟨a, h⟩, ⟨⟨a, h.fst⟩, h.snd⟩ },
id ┴ ┴ └──┘ └──┘
src ───┘└────┘ └┘ └┘ └─┘ └┘ └──┘└─┘ └──┘└┘└──
typ ─────────┘ └┘┴└┘┴└─┘ └┘ └──┘└─┘ └──┘└────
doc ───┘└────┘ └┘ └┘ └─┘ └┘ └─┘ └┘└──
txt ───┘└────┘ └┘ └┘ └─┘ └┘ └─┘ └┘└──
par ─────────┘ └┘ └┘ └─┘ └┘ └─┘ └────
pid ─────────┘ └┘ └┘ └─┘ └┘ └─┘ └────
st ──┘└───────────────────────────────────┘┴└─
240 { exact λ ⟨a, ha⟩ ⟨b, hb⟩ h,
src ───┘└────┘ └┘ └┘ └─┘ └┘ └────
typ ─────────┘ └┘ └┘ └─┘ └┘ └────
doc ───┘└────┘ └┘ └┘ └─┘ └┘ └────
txt ───┘└────┘ └┘ └┘ └─┘ └┘ └────
par ─────────┘ └┘ └┘ └─┘ └┘ └────
pid ─────────┘ └┘ └┘ └─┘ └┘ └────
st ───────────────────────────────
241 by injection h with h; congr; injection h },
id ┴ ┴
src ─────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴└──
typ ─────┘ ┴└────────┘┴└─────┘└┘└───┘└┘└────────┘┴┴└──
doc ─────┘ ┴└────────┘ └─────┘└┘ └┘└────────┘ ┴└──
txt ─────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴└──
par ─────┘ ┴└────────┘ └─────┘└┘└───┘└┘└────────┘ ┴└──
pid ─────┘ └─────────┘ └────────────────────────┘ └───
st ───────┘└──────────────────────────────────────┘└──
242 end
src ────
typ ────
doc ────
txt ────
par ────
pid ──┘└
st ──┘└
243
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
244 theorem omega_le_cof {o} : cardinal.omega ≤ cof o ↔ is_limit o :=
id └────────────┘ ┴ └─┘ ┴ ┴ └──────┘ ┴
src └────────────┘ ┴ └─┘ ┴ └──────┘
typ └────────────┘ ┴ └─┘ ┴ ┴ └──────┘ ┴
doc └────────────┘ └─┘ └──────┘
245 begin
st └─────
246 rcases zero_or_succ_or_limit o with rfl|⟨o,rfl⟩|l,
id └───────────────────┘ ┴
src └─────┘└───────────────────┘┴ └─────────────────┘
typ └─────┘└───────────────────┘┴┴└─────────────────┘
doc └─────┘ ┴ └─────────────────┘
txt └─────┘ ┴ └─────────────────┘
par └─────┘ ┴ └─────────────────┘
pid ┴ ┴ └─────────────────┘
st ──────────────────────────────────────────────────┘└─
247 { simp [not_zero_is_limit, cardinal.omega_ne_zero] },
id └───────────────┘ └────────────────────┘
src └────┘└───────────────┘└┘└────────────────────┘└┘
typ └────┘└───────────────┘└┘└────────────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───┘└───────────────────────────────────────────────┘└┘└
248 { simp [not_succ_is_limit, cardinal.one_lt_omega] },
id └───────────────┘ └───────────────────┘
src └────┘└───────────────┘└┘└───────────────────┘└┘
typ └────┘└───────────────┘└┘└───────────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───┘└──────────────────────────────────────────────┘└┘└
249 { simp [l], refine le_of_not_lt (λ h, _),
id ┴ └──────────┘
src └────┘ ┴ └─────┘└──────────┘┴ └────┘
typ └────┘┴┴ └─────┘└──────────┘┴ └────┘
doc └────┘ ┴ └─────┘ ┴ └────┘
txt └────┘ ┴ └─────┘ ┴ └────┘
par └────┘ ┴ └─────┘ ┴ └────┘
pid ┴┴ ┴ ┴ ┴ └────┘
st ───────────┘└────────────────────────────┘└─
250 cases cardinal.lt_omega.1 h with n e,
id └───────────────┘ ┴
src └────┘└───────────────┘└─┘ └───────┘
typ └────┘└───────────────┘└─┘┴└───────┘
doc └────┘ └─┘ └───────┘
txt └────┘ └─┘ └───────┘
par └────┘ └─┘ └───────┘
pid ┴ └─┘ └───────┘
st ───────────────────────────────────────┘└─
251 have := cof_cof o,
id └─────┘ ┴
src └──────┘└─────┘┴
typ └──────┘└─────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ────────────────────┘└─
252 rw [e, ord_nat] at this,
id ┴ └─────┘
src └──┘ └┘└─────┘└───────┘
typ └──┘┴└┘└─────┘└───────┘
doc └──┘ └┘ └───────┘
txt └──┘ └┘ └───────┘
par └──┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ────────┘└───────┘┴└──────┘└─
253 cases n,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
254 { simp at e, simpa [e, not_zero_is_limit] using l },
id ┴ └───────────────┘ ┴
src └───────┘ └─────┘ └┘└───────────────┘└──────┘ ┴
typ └───────┘ └─────┘┴└┘└───────────────┘└──────┘┴┴
doc └───────┘ └─────┘ └┘ └──────┘ ┴
txt └───────┘ └─────┘ └┘ └──────┘ ┴
par └───────┘ └─────┘ └┘ └──────┘ ┴
pid ┴└──┘ ┴┴ └┘ ┴┴└────┘ ┴
st ─────┘└───────┘└─────────────────────────────────────┘└┘└
255 { rw [← nat_cast_succ, cof_succ] at this,
id └───────────┘ └──────┘
src └────┘└───────────┘└┘└──────┘└───────┘
typ └────┘└───────────┘└┘└──────┘└───────┘
doc └────┘ └┘ └───────┘
txt └────┘ └┘ └───────┘
par └────┘ └┘ └───────┘
pid └──┘ └┘ ┴└──────┘
st ────────────────────────┘└────────┘┴└──────┘└─
256 rw [← this, cof_eq_one_iff_is_succ] at e,
id └──┘ └────────────────────┘
src └────┘ └┘└────────────────────┘└────┘
typ └────┘└──┘└┘└────────────────────┘└────┘
doc └────┘ └┘ └────┘
txt └────┘ └┘ └────┘
par └────┘ └┘ └────┘
pid └──┘ └┘ ┴└───┘
st ───────────────┘└──────────────────────┘┴└───┘└─
257 rcases e with ⟨a, rfl⟩,
id ┴
src └─────┘ └────────────┘
typ └─────┘┴└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ───────────────────────────┘└─
258 exact not_succ_is_limit _ l } }
id └───────────────┘ ┴
src └────┘└───────────────┘└─┘ ┴
typ └────┘└───────────────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────┘└───
259 end
st ──┘
260
261 @[simp] theorem cof_omega : cof omega = cardinal.omega :=
id └─┘ └───┘ ┴ └────────────┘
src └─┘ └───┘ ┴ └────────────┘
typ └─┘ └───┘ ┴ └────────────┘
doc └──┘ └─┘ └───┘ └────────────┘
262 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
263 (by rw ← card_omega; apply cof_le_card)
id └────────┘ └─────────┘
src └───┘└────────┘ └────┘└─────────┘
typ └───┘└────────┘ └────┘└─────────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ ┴
st └─────────────────────────────────┘
264 (omega_le_cof.2 omega_is_limit)
id └──────────┘┴ └────────────┘
src └──────────┘┴ └────────────┘
typ └──────────┘┴ └────────────┘
265
266 theorem cof_eq' (r : α → α → Prop) [is_well_order α r] (h : is_limit (type r)) :
id ┴ ┴ └───────────┘ ┴ ┴ └──────┘ └──┘ ┴
src └───────────┘ └──────┘ └──┘
typ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ └──┘ ┴
doc └───────────┘ └──────┘ └──┘
267 ∃ S : set α, (∀ a, ∃ b ∈ S, r a b) ∧ mk S = cof (type r) :=
id ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └──┘
typ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └──┘ ┴
doc └┘ └─┘ └──┘
268 let ⟨S, H, e⟩ := cof_eq r in
id └─┘ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ └─┘ ┴ ┴ ┴ └────┘ ┴
269 ⟨S, λ a,
id ┴
typ ┴
270 let a' := enum r _ (h.2 _ (typein_lt_type r a)) in
id └┘ └──┘ ┴ ┴┴ └────────────┘ ┴ ┴
src └──┘ ┴ └────────────┘
typ └┘ └──┘ ┴ ┴┴ └────────────┘ ┴ ┴
doc └──┘
271 let ⟨b, h, ab⟩ := H a' in
id └─┘ ┴ ┴ └┘ └┘
typ └─┘ ┴ ┴ └┘ └┘
272 ⟨b, h, (is_order_connected.conn a b a' $ (typein_lt_typein r).1
id └─────────────────────┘ ┴ └┘ └──────────────┘ ┴ ┴
src └─────────────────────┘ └──────────────┘ ┴
typ └─────────────────────┘ ┴ └┘ └──────────────┘ ┴ ┴
273 (by rw typein_enum; apply ordinal.lt_succ_self)).resolve_right ab⟩,
id └─────────┘ └──────────────────┘ └───────────┘
src └─┘└─────────┘ └────┘└──────────────────┘ └───────────┘
typ └─┘└─────────┘ └────┘└──────────────────┘ └───────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────────────────────┘
274 e⟩
275
276 theorem cof_sup_le_lift {ι} (f : ι → ordinal) (H : ∀ i, f i < sup f) :
id ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─────┘ └─┘
277 cof (sup f) ≤ (mk ι).lift :=
id └─┘ └─┘ ┴ ┴ └┘ ┴ └──┘
src └─┘ └─┘ ┴ └┘ └──┘
typ └─┘ └─┘ ┴ ┴ └┘ ┴ └──┘
doc └─┘ └─┘ └┘ └──┘
278 begin
st └─────
279 generalize e : sup f = o,
id └─┘ ┴
src └─────────────┘└─┘┴ ┴ ┴
typ └─────────────┘└─┘┴┴┴ ┴
doc └─────────────┘└─┘┴ ┴ ┴
txt └─────────────┘ ┴ ┴ ┴
par └─────────────┘ ┴ ┴ ┴
pid └┘└┘┴ ┴ ┴ ┴
st ─────────────────────────┘└─
280 refine ordinal.induction_on o _ e, introsI α r _ e',
id └──────────────────┘ ┴ ┴
src └─────┘└──────────────────┘┴ └─┘ └──────────────┘
typ └─────┘└──────────────────┘┴┴└─┘┴ └──────────────┘
doc └─────┘ ┴ └─┘ └──────────────┘
txt └─────┘ ┴ └─┘ └──────────────┘
par └─────┘ ┴ └─┘ └──────────────┘
pid ┴ ┴ └─┘ └───────┘
st ──────────────────────────────────┘└────────────────┘└─
281 rw e' at H,
id └┘
src └─┘ └───┘
typ └─┘└┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────┘└─
282 refine le_trans (cof_type_le (set.range (λ i, enum r _ (H i))) _)
id └──────┘ └─────────┘ └───────┘ └──┘ ┴ ┴
src └─────┘└──────┘┴ └─────────┘┴ └───────┘┴ └──┘└──┘┴ └─┘ ┴ └──────
typ └─────┘└──────┘┴ └─────────┘┴ └───────┘┴ └──┘└──┘┴┴└─┘ ┴┴ └──────
doc └─────┘ ┴ ┴ └───────┘┴ └──┘└──┘┴ └─┘ ┴ └──────
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └──────
par └─────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └──────
pid ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └──────
st ────────────────────────────────────────────────────────────────────
283 ⟨embedding.of_surjective _⟩,
id └─────────────────────┘
src ───┘ └─────────────────────┘└─┘
typ ───┘ └─────────────────────┘└─┘
doc ───┘ └─┘
txt ───┘ └─┘
par ───┘ └─┘
pid ───┘ └─┘
st ──────────────────────────────┘└─
284 { intro a, by_contra h,
src └─────┘ └─────────┘
typ └─────┘ └─────────┘
doc └─────┘ └─────────┘
txt └─────┘ └─────────┘
par └─────┘ └─────────┘
pid └┘ └┘
st ───┘└─────┘└───────────┘└─
285 apply not_le_of_lt (typein_lt_type r a),
id └──────────┘ └────────────┘ ┴ ┴
src └────┘└──────────┘┴ └────────────┘┴ ┴ ┴
typ └────┘└──────────┘┴ └────────────┘┴┴┴┴┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
286 rw [← e', sup_le],
id └┘ └────┘
src └────┘ └┘└────┘┴
typ └────┘└┘└┘└────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ───────────┘└──────┘└──
287 intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
288 simp [set.range] at h,
id └───────┘
src └────┘└───────┘└────┘
typ └────┘└───────┘└────┘
doc └────┘└───────┘└────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴┴ ┴┴└──┘
st ────────────────────────┘└─
289 simpa using le_of_lt ((typein_lt_typein r).2 (h _ i rfl)) },
id └──────┘ └──────────────┘ ┴ ┴ ┴ └─┘
src └──────────┘└──────┘┴ └──────────────┘┴ └──┘ └─┘ ┴└─┘└─┘
typ └──────────┘└──────┘┴ └──────────────┘┴┴└──┘ ┴└─┘┴┴└─┘└─┘
doc └──────────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
txt └──────────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
par └──────────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
pid ┴└────┘ ┴ ┴ └──┘ └─┘ ┴ └┘┴
st ─────────────────────────────────────────────────────────────┘└┘└
290 { exact λ i, ⟨_, set.mem_range_self i.1⟩ },
id └────────────────┘
src └────┘ └──┘ └─┘└────────────────┘┴ └──┘
typ └────┘ └──┘ └─┘└────────────────┘┴ └──┘
doc └────┘ └──┘ └─┘ ┴ └──┘
txt └────┘ └──┘ └─┘ ┴ └──┘
par └────┘ └──┘ └─┘ ┴ └──┘
pid ┴ └──┘ └─┘ ┴ └─┘┴
st ───┘└─────────────────────────────────────┘└┘└
291 { intro a, rcases a with ⟨_, i, rfl⟩, exact ⟨⟨i⟩, by simp⟩ }
id ┴ ┴
src └─────┘ └─────┘ └───────────────┘ └────┘ └─┘ ┴└──┘└┘
typ └─────┘ └─────┘┴└───────────────┘ └────┘ ┴└─┘ ┴└──┘└┘
doc └─────┘ └─────┘ └───────────────┘ └────┘ └─┘ ┴└──┘└┘
txt └─────┘ └─────┘ └───────────────┘ └────┘ └─┘ ┴└──┘└┘
par └─────┘ └─────┘ └───────────────┘ └────┘ └─┘ ┴└──┘└┘
pid └┘ ┴ └───────────────┘ ┴ └─┘ └────┘┴
st ──────────┘└─────────────────────────┘└──────────────┘└───┘└┘└─
292 end
st ──┘
293
294 theorem cof_sup_le {ι} (f : ι → ordinal) (H : ∀ i, f i < sup.{u u} f) :
id ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ ┴ └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─────┘ └─┘
295 cof (sup.{u u} f) ≤ mk ι :=
id └─┘ └─┘ ┴ ┴ └┘ ┴
src └─┘ └─┘ ┴ └┘
typ └─┘ └─┘ ┴ ┴ └┘ ┴
doc └─┘ └─┘ └┘
296 by simpa using cof_sup_le_lift.{u u} f H
id └─────────────┘ ┴ ┴
src └──────────┘└─────────────┘└─────┘ ┴ └
typ └──────────┘└─────────────┘└─────┘┴┴┴└
doc └──────────┘ └─────┘ ┴ └
txt └──────────┘ └─────┘ ┴ └
par └──────────┘ └─────┘ ┴ └
pid ┴└────┘ └─────┘ ┴ └
st └──────────────────────────────────────
297
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
298 theorem cof_bsup_le_lift {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup o f) →
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ └──┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─────┘ └─────┘ └──┘
299 cof (bsup o f) ≤ o.card.lift :=
id └─┘ └──┘ ┴ ┴ ┴ ┴└───┘└───┘
src └─┘ └──┘ ┴ └───┘└───┘
typ └─┘ └──┘ ┴ ┴ ┴ ┴└───┘└───┘
doc └─┘ └──┘ └───┘└───┘
300 induction_on o $ λ α r _ f H,
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
301 by rw bsup_type; refine cof_sup_le_lift _ _;
id └───────┘ └─────────────┘
src └─┘└───────┘ └─────┘└─────────────┘└──┘
typ └─┘└───────┘ └─────┘└─────────────┘└──┘
doc └─┘ └─────┘ └──┘
txt └─┘ └─────┘ └──┘
par └─┘ └─────┘ └──┘
pid ┴ ┴ └──┘
st └──────────────────────────────────────────
302 rw ← bsup_type; intro a; apply H
id └───────┘
src └───┘└───────┘ └─────┘ └────┘ └
typ └───┘└───────┘ └─────┘ └────┘ └
doc └───┘ └─────┘ └────┘ └
txt └───┘ └─────┘ └────┘ └
par └───┘ └─────┘ └────┘ └
pid └─┘ └┘ ┴ └
st ────────────────────────────────────
303
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
304 theorem cof_bsup_le {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup.{u u} o f) →
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ └─────┘ ┴ └──┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─────┘ └─────┘ └──┘
305 cof (bsup.{u u} o f) ≤ o.card :=
id └─┘ └──┘ ┴ ┴ ┴ ┴└───┘
src └─┘ └──┘ ┴ └───┘
typ └─┘ └──┘ ┴ ┴ ┴ ┴└───┘
doc └─┘ └──┘ └───┘
306 induction_on o $ λ α r _ f H,
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
307 by simpa using cof_bsup_le_lift.{u u} f H
id └──────────────┘ ┴ ┴
src └──────────┘└──────────────┘└─────┘ ┴ └
typ └──────────┘└──────────────┘└─────┘┴┴┴└
doc └──────────┘ └─────┘ ┴ └
txt └──────────┘ └─────┘ ┴ └
par └──────────┘ └─────┘ ┴ └
pid ┴└────┘ └─────┘ ┴ └
st └───────────────────────────────────────
308
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
309 @[simp] theorem cof_univ : cof univ.{u v} = cardinal.univ :=
id └─┘ └──┘ ┴ └───────────┘
src └─┘ └──┘ ┴ └───────────┘
typ └─┘ └──┘ ┴ └───────────┘
doc └──┘ └─┘ └──┘ └───────────┘
310 le_antisymm (cof_le_card _) begin
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
st └─────
311 refine le_of_forall_lt (λ c h, _),
id └─────────────┘
src └─────┘└─────────────┘┴ └──────┘
typ └─────┘└─────────────┘┴ └──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ──────────────────────────────────┘└─
312 rcases lt_univ'.1 h with ⟨c, rfl⟩,
id └──────┘ ┴
src └─────┘└──────┘└─┘ └────────────┘
typ └─────┘└──────┘└─┘┴└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ──────────────────────────────────┘└─
313 rcases @cof_eq ordinal.{u} (<) _ with ⟨S, H, Se⟩,
id └────┘ └─────┘ ┴
src └─────┘ └────┘┴└─────┘└───┘┴└──────────────────┘
typ └─────┘ └────┘┴└─────┘└───┘┴└──────────────────┘
doc └─────┘ ┴└─────┘└───┘ └──────────────────┘
txt └─────┘ ┴ └───┘ └──────────────────┘
par └─────┘ ┴ └───┘ └──────────────────┘
pid ┴ ┴ └───┘ └──────────────────┘
st ─────────────────────────────────────────────────┘└─
314 rw [univ, ← lift_cof, ← cardinal.lift_lift, cardinal.lift_lt, ← Se],
id └──┘ └──────┘ └────────────────┘ └──────────────┘ └┘
src └──┘└──┘└──┘└──────┘└──┘└────────────────┘└┘└──────────────┘└──┘ ┴
typ └──┘└──┘└──┘└──────┘└──┘└────────────────┘└┘└──────────────┘└──┘└┘┴
doc └──┘└──┘└──┘ └──┘ └┘ └──┘ ┴
txt └──┘ └──┘ └──┘ └┘ └──┘ ┴
par └──┘ └──┘ └──┘ └┘ └──┘ ┴
pid └┘ └──┘ └──┘ └┘ └──┘ ┴
st ─────────┘└──────────┘└────────────────────┘└────────────────┘└────┘└──
315 refine lt_of_not_ge (λ h, _),
id └──────────┘
src └─────┘└──────────┘┴ └────┘
typ └─────┘└──────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ─────────────────────────────┘└─
316 cases cardinal.lift_down h with a e,
id └────────────────┘ ┴
src └────┘└────────────────┘┴ └───────┘
typ └────┘└────────────────┘┴┴└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ────────────────────────────────────┘└─
317 refine quotient.induction_on a (λ α e, _) e,
id └───────────────────┘ ┴ ┴
src └─────┘└───────────────────┘┴ ┴ └───────┘
typ └─────┘└───────────────────┘┴┴┴ └───────┘┴
doc └─────┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ────────────────────────────────────────────┘└─
318 cases quotient.exact e with f,
id └────────────┘ ┴
src └────┘└────────────┘┴ └─────┘
typ └────┘└────────────┘┴┴└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────────┘└─
319 have f := equiv.ulift.symm.trans f,
id └────────────────────┘ ┴
src └────────┘└────────────────────┘┴
typ └────────┘└────────────────────┘┴┴
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ───────────────────────────────────┘└─
320 let g := λ a, (f a).1,
id ┴
src └───────┘ └──┘ ┴ └─┘
typ └───────┘ └──┘ ┴┴ └─┘
doc └───────┘ └──┘ ┴ └─┘
txt └───────┘ └──┘ ┴ └─┘
par └───────┘ └──┘ ┴ └─┘
pid └───┘┴└─┘ └──┘ ┴ ┴└┘
st ──────────────────────┘└─
321 let o := succ (sup.{u u} g),
id └──┘ └─┘ ┴
src └───────┘└──┘┴ └─┘└─────┘ ┴
typ └───────┘└──┘┴ └─┘└─────┘┴┴
doc └───────┘└──┘┴ └─┘└─────┘ ┴
txt └───────┘ ┴ └─────┘ ┴
par └───────┘ ┴ └─────┘ ┴
pid └───┘┴└─┘ ┴ └─────┘ ┴
st ────────────────────────────┘└─
322 rcases H o with ⟨b, h, l⟩,
id ┴ ┴
src └─────┘ ┴ └─────────────┘
typ └─────┘┴┴┴└─────────────┘
doc └─────┘ ┴ └─────────────┘
txt └─────┘ ┴ └─────────────┘
par └─────┘ ┴ └─────────────┘
pid ┴ ┴ └─────────────┘
st ──────────────────────────┘└─
323 refine l (lt_succ.2 _),
id ┴ └─────┘
src └─────┘ ┴ └─────┘└───┘
typ └─────┘┴┴ └─────┘└───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ───────────────────────┘└─
324 rw ← show g (f.symm ⟨b, h⟩) = b, by dsimp [g]; simp,
id ┴ └────┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └────┘┴ └┘ └─┘┴┴ └───┘└─────┘ ┴└┘└──┘
typ └───┘ ┴┴┴ └────┘┴ └┘┴└─┘┴┴┴└───┘└─────┘┴┴└┘└──┘
doc └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ └───┘└─────┘ ┴└┘└──┘
txt └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ └───┘└─────┘ ┴└┘└──┘
par └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ └───┘└─────┘ ┴└┘└──┘
pid └─┘ ┴ ┴ ┴ └┘ └─┘ ┴ └──────────┘ └─────┘
st ────────────────────────────────────┘└──────────────┘└─
325 apply le_sup
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────┘
326 end
st └─┘
327
328 theorem sup_lt_ord {ι} (f : ι → ordinal) {c : ordinal} (H1 : cardinal.mk ι < c.cof)
id ┴ └─────┘ └─────┘ └─────────┘ ┴ ┴ ┴└──┘
src └─────┘ └─────┘ └─────────┘ ┴ └──┘
typ ┴ └─────┘ └─────┘ └─────────┘ ┴ ┴ ┴└──┘
doc └─────┘ └─────┘ └─────────┘ └──┘
329 (H2 : ∀ i, f i < c) : sup.{u u} f < c :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
330 begin
st └─────
331 apply lt_of_le_of_ne,
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
332 { rw [sup_le], exact λ i, le_of_lt (H2 i) },
id └────┘ └──────┘ └┘
src └──┘└────┘┴ └────┘ └──┘└──────┘┴ ┴ └┘
typ └──┘└────┘┴ └────┘ └──┘└──────┘┴ └┘┴ └┘
doc └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘
txt └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘
par └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └──┘ ┴ ┴ ┴┴
st ───┘└────────┘└────────────────────────────┘└┘└
333 rintro h, apply not_le_of_lt H1,
id └──────────┘ └┘
src └──────┘ └────┘└──────────┘┴
typ └──────┘ └────┘└──────────┘┴└┘
doc └──────┘ └────┘ ┴
txt └──────┘ └────┘ ┴
par └──────┘ └────┘ ┴
pid └┘ ┴ ┴
st ─────────┘└─────────────────────┘└─
334 simpa [sup_ord, H2, h] using cof_sup_le.{u} f
id └─────┘ └┘ ┴ └────────┘ ┴
src └─────┘└─────┘└┘ └┘ └──────┘└────────┘└───┘ ┴
typ └─────┘└─────┘└┘└┘└┘┴└──────┘└────────┘└───┘┴┴
doc └─────┘ └┘ └┘ └──────┘ └───┘ ┴
txt └─────┘ └┘ └┘ └──────┘ └───┘ ┴
par └─────┘ └┘ └┘ └──────┘ └───┘ ┴
pid ┴┴ └┘ └┘ ┴┴└────┘ └───┘ ┴
st ───────────────────────────────────────────────┘
335 end
st └─┘
336
337 theorem sup_lt {ι} (f : ι → cardinal) {c : cardinal} (H1 : cardinal.mk ι < c.ord.cof)
id ┴ └──────┘ └──────┘ └─────────┘ ┴ ┴ ┴└──┘└──┘
src └──────┘ └──────┘ └─────────┘ ┴ └──┘└──┘
typ ┴ └──────┘ └──────┘ └─────────┘ ┴ ┴ ┴└──┘└──┘
doc └──────┘ └──────┘ └─────────┘ └──┘└──┘
338 (H2 : ∀ i, f i < c) : cardinal.sup.{u u} f < c :=
id ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └──────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
339 by { rw [←ord_lt_ord, ←sup_ord], apply sup_lt_ord _ H1, intro i, rw ord_lt_ord, apply H2 }
id └────────┘ └─────┘ └────────┘ └┘ └────────┘
src └───┘└────────┘└─┘└─────┘┴ └────┘└────────┘└─┘ └─────┘ └─┘└────────┘ └────┘ ┴
typ └───┘└────────┘└─┘└─────┘┴ └────┘└────────┘└─┘└┘ └─────┘ └─┘└────────┘ └────┘ ┴
doc └───┘ └─┘ ┴ └────┘ └─┘ └─────┘ └─┘ └────┘ ┴
txt └───┘ └─┘ ┴ └────┘ └─┘ └─────┘ └─┘ └────┘ ┴
par └───┘ └─┘ ┴ └────┘ └─┘ └─────┘ └─┘ └────┘ ┴
pid └─┘ └─┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴
st └────────────────┘└────────┘└──────────────────────┘└───────┘└─────────────┘└─────────┘└┘
340
341 /-- If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member -/
342 theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : is_well_order α r] {s : set (set α)}
id ┴ ┴ └───────────┘ ┴ ┴ └─┘ └─┘ ┴
src └───────────┘ └─┘ └─┘
typ ┴ ┴ └───────────┘ ┴ ┴ └─┘ └─┘ ┴
doc └───────────┘
343 (h₁ : unbounded r $ ⋃₀ s) (h₂ : mk s < strict_order.cof r) : ∃(x ∈ s), unbounded r x :=
id └───────┘ ┴ └┘ ┴ └┘ ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └┘ └┘ ┴ └──────────────┘ ┴ ┴ └───────┘
typ └───────┘ ┴ └┘ ┴ └┘ ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └┘ └───────┘
344 begin
st └─────
345 by_contra h, simp only [not_exists, exists_prop, not_and, not_unbounded_iff] at h,
id └────────┘ └─────────┘ └─────┘ └───────────────┘
src └─────────┘ └─────────┘└────────┘└┘└─────────┘└┘└─────┘└┘└───────────────┘└────┘
typ └─────────┘ └─────────┘└────────┘└┘└─────────┘└┘└─────┘└┘└───────────────┘└────┘
doc └─────────┘ └─────────┘ └┘ └┘ └┘ └────┘
txt └─────────┘ └─────────┘ └┘ └┘ └┘ └────┘
par └─────────┘ └─────────┘ └┘ └┘ └┘ └────┘
pid └┘ ┴└──┘└┘ └┘ └┘ └┘ ┴┴└──┘
st ────────────┘└────────────────────────────────────────────────────────────────────┘└─
346 apply not_le_of_lt h₂,
id └──────────┘ └┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────┘└─
347 let f : s → α := λ x : s, wo.wf.sup x (h x.1 x.2),
id ┴ ┴ ┴ └───────┘ ┴
src └──────┘ ┴ ┴ └──┘ └───┘ └┘└───────┘┴ ┴ ┴ └─┘ └─┘
typ └──────┘┴┴ ┴┴└──┘ └───┘┴└┘└───────┘┴ ┴ ┴┴ └─┘ └─┘
doc └──────┘ ┴ ┴ └──┘ └───┘ └┘ ┴ ┴ ┴ └─┘ └─┘
txt └──────┘ ┴ ┴ └──┘ └───┘ └┘ ┴ ┴ ┴ └─┘ └─┘
par └──────┘ ┴ ┴ └──┘ └───┘ └┘ ┴ ┴ ┴ └─┘ └─┘
pid └───┘└─┘ ┴ ┴ └──┘ └───┘ └┘ ┴ ┴ ┴ └─┘ └─┘
st ──────────────────────────────────────────────────┘└─
348 let t : set α := range f,
id └─┘ ┴ └───┘ ┴
src └──────┘└─┘┴ └──┘└───┘┴
typ └──────┘└─┘┴┴└──┘└───┘┴┴
doc └──────┘ ┴ └──┘└───┘┴
txt └──────┘ ┴ └──┘ ┴
par └──────┘ ┴ └──┘ ┴
pid └───┘└─┘ ┴ └──┘ ┴
st ─────────────────────────┘└─
349 have : mk t ≤ mk s, exact mk_range_le, refine le_trans _ this,
id ┴ ┴ └┘ ┴ └─────────┘ └──────┘ └──┘
src └─────┘ ┴ ┴┴┴└┘┴ └────┘└─────────┘ └─────┘└──────┘└─┘
typ └─────┘ ┴┴┴┴┴└┘┴┴ └────┘└─────────┘ └─────┘└──────┘└─┘└──┘
doc └─────┘ ┴ ┴ ┴└┘┴ └────┘ └─────┘ └─┘
txt └─────┘ ┴ ┴ ┴ ┴ └────┘ └─────┘ └─┘
par └─────┘ ┴ ┴ ┴ ┴ └────┘ └─────┘ └─┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ───────────────────┘└─────────────────┘└──────────────────────┘└─
350 have : unbounded r t,
id └───────┘ ┴ ┴
src └─────┘└───────┘┴ ┴
typ └─────┘└───────┘┴┴┴┴
doc └─────┘└───────┘┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴
st ─────────────────────┘└─
351 { intro x, rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩,
id └┘ ┴
src └─────┘ └─────┘ ┴ └─────────────────────────┘
typ └─────┘ └─────┘└┘┴┴└─────────────────────────┘
doc └─────┘ └─────┘ ┴ └─────────────────────────┘
txt └─────┘ └─────┘ ┴ └─────────────────────────┘
par └─────┘ └─────┘ ┴ └─────────────────────────┘
pid └┘ ┴ ┴ └─────────────────────────┘
st ───┘└─────┘└──────────────────────────────────────┘└─
352 refine ⟨f ⟨c, hc⟩, mem_range_self _, _⟩, intro hxz, apply hxy,
id ┴ ┴ └┘ └────────────┘
src └─────┘ ┴ └┘ └─┘└────────────┘└────┘ └───────┘ └────┘
typ └─────┘ ┴┴ ┴└┘└┘└─┘└────────────┘└────┘ └───────┘ └────┘
doc └─────┘ ┴ └┘ └─┘ └────┘ └───────┘ └────┘
txt └─────┘ ┴ └┘ └─┘ └────┘ └───────┘ └────┘
par └─────┘ ┴ └┘ └─┘ └────┘ └───────┘ └────┘
pid ┴ ┴ └┘ └─┘ └────┘ └──┘ ┴
st ──────────────────────────────────────────┘└─────────┘└─────────┘└─
353 refine trans (wo.wf.lt_sup _ hy) hxz },
id └───┘ └──────────┘ └┘ └─┘
src └─────┘└───┘┴ └──────────┘└─┘ └┘ ┴
typ └─────┘└───┘┴ └──────────┘└─┘└┘└┘└─┘┴
doc └─────┘ ┴ └─┘ └┘ ┴
txt └─────┘ ┴ └─┘ └┘ ┴
par └─────┘ ┴ └─┘ └┘ ┴
pid ┴ ┴ └─┘ └┘ ┴
st ────────────────────────────────────────┘└┘└
354 exact cardinal.min_le _ (subtype.mk t this)
id └─────────────┘ └────────┘ ┴ └──┘
src └────┘└─────────────┘└─┘ └────────┘┴ ┴ └┘
typ └────┘└─────────────┘└─┘ └────────┘┴┴┴└──┘└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────────────────┘
355 end
st └─┘
356
357 /-- If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member -/
358 theorem unbounded_of_unbounded_Union {α β : Type u} (r : α → α → Prop) [wo : is_well_order α r]
id ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
359 (s : β → set α)
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
360 (h₁ : unbounded r $ ⋃x, s x) (h₂ : mk β < strict_order.cof r) : ∃x : β, unbounded r (s x) :=
id └───────┘ ┴ ┴┴┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘ ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └┘ ┴ └──────────────┘ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴┴┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘ ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴
doc └───────┘ ┴ ┴ └┘ └───────┘
361 begin
st └─────
362 rw [← sUnion_range] at h₁,
id └──────────┘
src └────┘└──────────┘└─────┘
typ └────┘└──────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid └──┘ ┴└────┘
st ───────────────────┘┴└────┘└─
363 have : mk ↥(range (λ (i : β), s i)) < strict_order.cof r := lt_of_le_of_lt mk_range_le h₂,
id └┘ ┴ └───┘ ┴ ┴ ┴ └──────────────┘ ┴ └────────────┘ └─────────┘ └┘
src └─────┘└┘┴┴ └───┘┴ └────┘ └─┘ ┴ └─┘┴┴└──────────────┘┴ └──┘└────────────┘┴└─────────┘┴
typ └─────┘└┘┴┴ └───┘┴ └────┘┴└─┘┴┴ └─┘┴┴└──────────────┘┴┴└──┘└────────────┘┴└─────────┘┴└┘
doc └─────┘└┘┴ └───┘┴ └────┘ └─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
txt └─────┘ ┴ ┴ └────┘ └─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
par └─────┘ ┴ ┴ └────┘ └─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
pid └───┘└┘ ┴ ┴ └────┘ └─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
364 rcases unbounded_of_unbounded_sUnion r h₁ this with ⟨_, ⟨x, rfl⟩, u⟩, exact ⟨x, u⟩
id └───────────────────────────┘ ┴ └┘ └──┘ ┴ ┴
src └─────┘└───────────────────────────┘┴ ┴ ┴ └────────────────────┘ └────┘ └┘ └┘
typ └─────┘└───────────────────────────┘┴┴┴└┘┴└──┘└────────────────────┘ └────┘ ┴└┘┴└┘
doc └─────┘└───────────────────────────┘┴ ┴ ┴ └────────────────────┘ └────┘ └┘ └┘
txt └─────┘ ┴ ┴ ┴ └────────────────────┘ └────┘ └┘ └┘
par └─────┘ ┴ ┴ ┴ └────────────────────┘ └────┘ └┘ └┘
pid ┴ ┴ ┴ ┴ └────────────────────┘ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────────┘└─────────────┘
365 end
st └─┘
366
367 /-- The infinite pigeonhole principle-/
368 theorem infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : cardinal.omega ≤ mk β)
id ┴ ┴ └────────────┘ ┴ └┘ ┴
src └────────────┘ ┴ └┘
typ ┴ ┴ └────────────┘ ┴ └┘ ┴
doc └────────────┘ └┘
369 (h₂ : mk α < (mk β).ord.cof) : ∃a : α, mk (f ⁻¹' {a}) = mk β :=
id └┘ ┴ ┴ └┘ ┴ └─┘ └─┘ ┴ ┴┴ └┘ ┴ └─┘ ┴┴ ┴ └┘ ┴
src └┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘
typ └┘ ┴ ┴ └┘ ┴ └─┘ └─┘ ┴ ┴┴ └┘ ┴ └─┘ ┴┴ ┴ └┘ ┴
doc └┘ └┘ └─┘ └─┘ └┘ └─┘ └┘
370 begin
st └─────
371 have : ¬∀a, mk (f ⁻¹' {a}) < mk β,
id ┴ ┴ └─┘ ┴ ┴ └┘ ┴
src └─────┘┴ ┴ ┴ ┴ ┴└─┘┴┴└──┘┴┴└┘┴
typ └─────┘┴ ┴ ┴ ┴ ┴┴└─┘┴┴└──┘┴┴└┘┴┴
doc └─────┘ ┴ ┴ ┴ ┴└─┘┴ └──┘ ┴└┘┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────┘└─
372 { intro h,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
373 apply not_lt_of_ge (ge_of_eq $ mk_univ),
id └──────────┘ └──────┘ └─────┘
src └────┘└──────────┘┴ └──────┘┴ ┴└─────┘┴
typ └────┘└──────────┘┴ └──────┘┴ ┴└─────┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
374 rw [←@preimage_univ _ _ f, ←Union_of_singleton, preimage_Union],
id └───────────┘ ┴ └────────────────┘ └────────────┘
src └───┘ └───────────┘└───┘ └─┘└────────────────┘└┘└────────────┘┴
typ └───┘ └───────────┘└───┘┴└─┘└────────────────┘└┘└────────────┘┴
doc └───┘ └───┘ └─┘ └┘ ┴
txt └───┘ └───┘ └─┘ └┘ ┴
par └───┘ └───┘ └─┘ └┘ ┴
pid └─┘ └───┘ └─┘ └┘ ┴
st ────────────────────────────┘└───────────────────┘└──────────────┘└──
375 apply lt_of_le_of_lt mk_Union_le_sum_mk,
id └────────────┘ └────────────────┘
src └────┘└────────────┘┴└────────────────┘
typ └────┘└────────────┘┴└────────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────────┘└─
376 apply lt_of_le_of_lt (sum_le_sup _),
id └────────────┘ └────────┘
src └────┘└────────────┘┴ └────────┘└─┘
typ └────┘└────────────┘┴ └────────┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ──────────────────────────────────────┘└─
377 apply mul_lt_of_lt h₁ (lt_of_lt_of_le h₂ $ cof_ord_le _),
id └──────────┘ └┘ └────────────┘ └┘ └────────┘
src └────┘└──────────┘┴ ┴ └────────────┘┴ ┴ ┴└────────┘└─┘
typ └────┘└──────────┘┴└┘┴ └────────────┘┴└┘┴ ┴└────────┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────┘└─
378 exact sup_lt _ h₂ h },
id └────┘ └┘ ┴
src └────┘└────┘└─┘ ┴ ┴
typ └────┘└────┘└─┘└┘┴┴┴
doc └────┘ └─┘ ┴ ┴
txt └────┘ └─┘ ┴ ┴
par └────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────┘└┘└
379 rw [not_forall] at this, cases this with x h,
id └────────┘ └──┘
src └──┘└────────┘└───────┘ └────┘ └───────┘
typ └──┘└────────┘└───────┘ └────┘└──┘└───────┘
doc └──┘ └───────┘ └────┘ └───────┘
txt └──┘ └───────┘ └────┘ └───────┘
par └──┘ └───────┘ └────┘ └───────┘
pid └┘ ┴└──────┘ ┴ └───────┘
st ───────────────┘┴└──────┘└───────────────────┘└─
380 use x, apply le_antisymm _ (le_of_not_gt h),
id ┴ └─────────┘ └──────────┘ ┴
src └──┘ └────┘└─────────┘└─┘ └──────────┘┴ ┴
typ └──┘┴ └────┘└─────────┘└─┘ └──────────┘┴┴┴
doc └──┘ └────┘ └─┘ ┴ ┴
txt └──┘ └────┘ └─┘ ┴ ┴
par └──┘ └────┘ └─┘ ┴ ┴
pid ┴ ┴ └─┘ ┴ ┴
st ──────┘└────────────────────────────────────┘└─
381 rw [le_mk_iff_exists_set], exact ⟨_, rfl⟩
id └──────────────────┘ └─┘
src └──┘└──────────────────┘┴ └────┘ └─┘└─┘└┘
typ └──┘└──────────────────┘┴ └────┘ └─┘└─┘└┘
doc └──┘ ┴ └────┘ └─┘ └┘
txt └──┘ ┴ └────┘ └─┘ └┘
par └──┘ ┴ └────┘ └─┘ └┘
pid └┘ ┴ ┴ └─┘ ┴┴
st ─────────────────────────┘└────────────────┘
382 end
st └─┘
383
384 /-- pigeonhole principle for a cardinality below the cardinality of the domain -/
385 theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ mk β)
id ┴ ┴ └──────┘ ┴ ┴ └┘ ┴
src └──────┘ ┴ └┘
typ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴
doc └──────┘ └┘
386 (h₁ : cardinal.omega ≤ θ) (h₂ : mk α < θ.ord.cof) : ∃a : α, θ ≤ mk (f ⁻¹' {a}) :=
id └────────────┘ ┴ ┴ └┘ ┴ ┴ ┴└──┘└──┘ ┴ ┴┴ ┴ ┴ └┘ ┴ └─┘ ┴┴
src └────────────┘ ┴ └┘ ┴ └──┘└──┘ ┴ ┴ ┴ └┘ └─┘ ┴
typ └────────────┘ ┴ ┴ └┘ ┴ ┴ ┴└──┘└──┘ ┴ ┴┴ ┴ ┴ └┘ ┴ └─┘ ┴┴
doc └────────────┘ └┘ └──┘└──┘ └┘ └─┘
387 begin
st └─────
388 rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩,
id └──────────────────┘ └┘
src └─────┘└──────────────────┘└─┘ └────────────┘
typ └─────┘└──────────────────┘└─┘└┘└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ───────────────────────────────────────────────┘└─
389 cases infinite_pigeonhole (f ∘ subtype.val : s → α) h₁ h₂ with a ha,
id └─────────────────┘ ┴ ┴ └─────────┘ ┴ ┴ └┘ └┘
src └────┘└─────────────────┘┴ ┴┴┴└─────────┘└─┘ ┴ ┴ └┘ ┴ └────────┘
typ └────┘└─────────────────┘┴ ┴┴┴┴└─────────┘└─┘┴┴ ┴┴└┘└┘┴└┘└────────┘
doc └────┘└─────────────────┘┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └────────┘
txt └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └────────┘
par └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └────────┘
pid ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └────────┘
st ────────────────────────────────────────────────────────────────────┘└─
390 use a, rw [←ha, @preimage_comp _ _ _ subtype.val f],
id ┴ └┘ └───────────┘ └─────────┘ ┴
src └──┘ └───┘ └┘ └───────────┘└─────┘└─────────┘┴ ┴
typ └──┘┴ └───┘└┘└┘ └───────────┘└─────┘└─────────┘┴┴┴
doc └──┘ └───┘ └┘ └─────┘ ┴ ┴
txt └──┘ └───┘ └┘ └─────┘ ┴ ┴
par └──┘ └───┘ └┘ └─────┘ ┴ ┴
pid ┴ └─┘ └┘ └─────┘ ┴ ┴
st ──────┘└───────┘└──────────────────────────────────┘└──
391 apply mk_preimage_of_injective _ _ subtype.val_injective
id └──────────────────────┘ └───────────────────┘
src └────┘└──────────────────────┘└───┘└───────────────────┘┴
typ └────┘└──────────────────────┘└───┘└───────────────────┘┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ──────────────────────────────────────────────────────────┘
392 end
st └─┘
393
394 theorem infinite_pigeonhole_set {β α : Type u} {s : set β} (f : s → α) (θ : cardinal)
id └─┘ ┴ ┴ ┴ └──────┘
src └─┘ └──────┘
typ └─┘ ┴ ┴ ┴ └──────┘
doc └──────┘
395 (hθ : θ ≤ mk s) (h₁ : cardinal.omega ≤ θ) (h₂ : mk α < θ.ord.cof) :
id ┴ ┴ └┘ ┴ └────────────┘ ┴ ┴ └┘ ┴ ┴ ┴└──┘└──┘
src ┴ └┘ └────────────┘ ┴ └┘ ┴ └──┘└──┘
typ ┴ ┴ └┘ ┴ └────────────┘ ┴ ┴ └┘ ┴ ┴ ┴└──┘└──┘
doc └┘ └────────────┘ └┘ └──┘└──┘
396 ∃(a : α) (t : set β) (h : t ⊆ s), θ ≤ mk t ∧ ∀{{x}} (hx : x ∈ t), f ⟨x, h hx⟩ = a :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘
397 begin
st └─────
398 cases infinite_pigeonhole_card f θ hθ h₁ h₂ with a ha,
id └──────────────────────┘ ┴ ┴ └┘ └┘ └┘
src └────┘└──────────────────────┘┴ ┴ ┴ ┴ ┴ └────────┘
typ └────┘└──────────────────────┘┴┴┴┴┴└┘┴└┘┴└┘└────────┘
doc └────┘└──────────────────────┘┴ ┴ ┴ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ └────────┘
par └────┘ ┴ ┴ ┴ ┴ ┴ └────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └────────┘
st ──────────────────────────────────────────────────────┘└─
399 refine ⟨a, {x | ∃(h : x ∈ s), f ⟨x, h⟩ = a}, _, _, _⟩,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └┘┴└──┘┴└───┘ ┴┴┴ ┴┴┴ ┴ └┘ └┘┴┴ └─────────┘
typ └─────┘ └┘┴└──┘┴└───┘ ┴┴┴┴┴┴┴┴┴ └┘ └┘┴┴┴└─────────┘
doc └─────┘ └┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────────┘
txt └─────┘ └┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────────┘
par └─────┘ └┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────────┘
pid ┴ └┘ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────────┘
st ──────────────────────────────────────────────────────┘└─
400 { rintro x ⟨hx, hx'⟩, exact hx },
id └┘
src └────────────────┘ └────┘ ┴
typ └────────────────┘ └────┘└┘┴
doc └────────────────┘ └────┘ ┴
txt └────────────────┘ └────┘ ┴
par └────────────────┘ └────┘ ┴
pid └──────────┘ ┴ ┴
st ───┘└────────────────┘└─────────┘└┘└
401 { refine le_trans ha _, apply ge_of_eq, apply quotient.sound, constructor,
id └──────┘ └┘ └──────┘ └────────────┘
src └─────┘└──────┘┴ └┘ └────┘└──────┘ └────┘└────────────┘ └─────────┘
typ └─────┘└──────┘┴└┘└┘ └────┘└──────┘ └────┘└────────────┘ └─────────┘
doc └─────┘ ┴ └┘ └────┘ └────┘ └─────────┘
txt └─────┘ ┴ └┘ └────┘ └────┘ └─────────┘
par └─────┘ ┴ └┘ └────┘ └────┘ └─────────┘
pid ┴ ┴ └┘ ┴ ┴
st ───┘└──────────────────┘└──────────────┘└────────────────────┘└───────────┘└─
402 refine equiv.trans _ (equiv.subtype_subtype_equiv_subtype_exists _ _).symm,
id └─────────┘ └────────────────────────────────────────┘
src └─────┘└─────────┘└─┘ └────────────────────────────────────────┘└────────┘
typ └─────┘└─────────┘└─┘ └────────────────────────────────────────┘└────────┘
doc └─────┘ └─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └───────┘┴
st ─────────────────────────────────────────────────────────────────────────────┘└┘
403 simp only [set_coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_set_of_eq] },
st └┘
404 rintro x ⟨hx, hx'⟩, exact hx'
405 end
st └─┘
406
407 end ordinal
408
409 namespace cardinal
410 open ordinal
411
412 local infixr ^ := @pow cardinal.{u} cardinal cardinal.has_pow
id └──────┘ └────┘ └┘ └┘ └┘ └┘
src └──────┘ └────┘ └┘ └┘ └┘ └┘
typ └──────┘ └────┘ └┘ └┘ └┘ └┘
doc └──────┘ └────┘
413
414 /-- A cardinal is a limit if it is not zero or a successor
415 cardinal. Note that `ω` is a limit cardinal by this definition. -/
416 def is_limit (c : cardinal) : Prop :=
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └┘ └──┘
417 c ≠ 0 ∧ ∀ x < c, succ x < c
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
418
419 /-- A cardinal is a strong limit if it is not zero and it is
420 closed under powersets. Note that `ω` is a strong limit by this definition. -/
421 def is_strong_limit (c : cardinal) : Prop :=
id ┴ └┘ └┘
src ┴ └┘ └┘
typ ┴ └┘ └┘
doc ┴ └┘ └┘
422 c ≠ 0 ∧ ∀ x < c, 2 ^ x < c
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
423
424 theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
id ┴ └┘ └┘ └┘ ┴ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ └┘ └┘ ┴
doc ┴ └┘ └┘ └┘ └┘ └┘
425 ⟨H.1, λ x h, lt_of_le_of_lt (succ_le.2 $ cantor _) (H.2 _ h)⟩
id ┴ ┴ ┴
typ ┴ ┴ ┴
426
427 /-- A cardinal is regular if it is infinite and it equals its own cofinality. -/
428 def is_regular (c : cardinal) : Prop :=
id └──┘
src └──┘
typ └──┘
doc └──┘
429 omega ≤ c ∧ c.ord.cof = c
id └───┘ ┴ ┴ ┴ └┘ └┘ ┴
src └───┘ ┴ └┘ └┘
typ └───┘ ┴ ┴ ┴ └┘ └┘ ┴
doc └───┘ └┘ └┘
430
431 theorem cof_is_regular {o : ordinal} (h : o.is_limit) : is_regular o.cof :=
id └┘ └┘ ┴└┘ └┘ └┘ └┘ └┘ ┴ ┴┴ ┴
src └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴
typ └┘ └┘ ┴└┘ └┘ └┘ └┘ └┘ ┴ ┴┴ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴
432 ⟨omega_le_cof.2 h, cof_cof _⟩
id ┴
typ ┴
433
434 theorem omega_is_regular : is_regular omega :=
id ┴ └┘ └┘ └───┘
src ┴ └┘ └┘ └───┘
typ ┴ └┘ └┘ └───┘
doc ┴ └┘ └┘ └───┘
435 ⟨le_refl _, by simp⟩
436
437 theorem succ_is_regular {c : cardinal.{u}} (h : omega ≤ c) : is_regular (succ c) :=
id └──┘ └┘ └──┘ └┘ └┘ └┘
src └──┘ └┘ └──┘ └┘ └┘ └┘
typ └──┘ └┘ └──┘ └┘ └┘ └┘
doc └──┘ └┘ └──┘ └┘ └┘ └┘
438 ⟨le_trans h (le_of_lt $ lt_succ_self _), begin
439 refine le_antisymm (cof_ord_le _) (succ_le.2 _),
440 cases quotient.exists_rep (succ c) with α αe, simp at αe,
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
441 rcases ord_eq α with ⟨r, wo, re⟩, resetI,
id ┴
typ ┴
442 have := ord_is_limit (le_trans h $ le_of_lt $ lt_succ_self _),
443 rw [← αe, re] at this ⊢,
444 rcases cof_eq' r this with ⟨S, H, Se⟩,
id ┴ └──┘
typ ┴ └──┘
445 rw [← Se],
446 apply lt_imp_lt_of_le_imp_le (mul_le_mul_right c),
id ┴
typ ┴
447 rw [mul_eq_self h, ← succ_le, ← αe, ← sum_const],
448 refine le_trans _ (sum_le_sum (λ x:S, card (typein r x)) _ _),
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
449 { simp [typein, sum_mk (λ x:S, {a//r a x})],
id ┴ ┴
typ ┴ ┴
450 refine ⟨embedding.of_surjective _⟩,
451 { exact λ x, x.2.1 },
st └┘
452 { exact λ a, let ⟨b, h, ab⟩ := H a in ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩ } },
id ┴ └┘
typ ┴ └┘
st └──┘
453 { intro i,
454 rw [← lt_succ, ← lt_ord, ← αe, re],
455 apply typein_lt_type }
st └─
456 end⟩
st ──┘
457
458 theorem sup_lt_ord_of_is_regular {ι} (f : ι → ordinal)
id ┴ └┘ └─┘
src └┘ └─┘
typ ┴ └┘ └─┘
doc └┘ └─┘
459 {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴
src └┘ └┘ ┴ └┘ └┘ └┘
typ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ └┘
460 (H2 : ∀ i, f i < c.ord) : ordinal.sup.{u u} f < c.ord :=
id ┴ ┴ ┴ ┴└─┘ ┴ ┴ └┘
src └─┘ └┘
typ ┴ ┴ ┴ ┴└─┘ ┴ ┴ └┘
doc └─┘ └┘
461 by { apply sup_lt_ord _ _ H2, rw [hc.2], exact H1 }
st └┘
462
463 theorem sup_lt_of_is_regular {ι} (f : ι → cardinal)
id ┴ └┘ └──┘
src └┘ └──┘
typ ┴ └┘ └──┘
doc └┘ └──┘
464 {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘
465 (H2 : ∀ i, f i < c) : sup.{u u} f < c :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
466 by { apply sup_lt _ _ H2, rwa [hc.2] }
st └┘
467
468 theorem sum_lt_of_is_regular {ι} (f : ι → cardinal)
id ┴ └┘ └──┘
src └┘ └──┘
typ ┴ └┘ └──┘
doc └┘ └──┘
469 {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘
470 (H2 : ∀ i, f i < c) : sum.{u u} f < c :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
471 lt_of_le_of_lt (sum_le_sup _) $ mul_lt_of_lt hc.1 H1 $
id └┘
typ └┘
472 sup_lt_of_is_regular f hc H1 H2
id ┴ └┘
typ ┴ └┘
473
474 /-- A cardinal is inaccessible if it is an
475 uncountable regular strong limit cardinal. -/
476 def is_inaccessible (c : cardinal) :=
id └┘ └┘ └┘
src └┘ └┘ └┘
typ └┘ └┘ └┘
doc └┘ └┘ └┘
477 omega < c ∧ is_regular c ∧ is_strong_limit c
id ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴
src ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴
doc ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
478
479 theorem is_inaccessible.mk {c}
480 (h₁ : omega < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, 2 ^ x < c) :
id └───┘ ┴ ┴ ┴└┘ └┘ ┴ ┴ ┴
src └───┘ └┘ └┘
typ └───┘ ┴ ┴ ┴└┘ └┘ ┴ ┴ ┴
doc └───┘ └┘ └┘
481 is_inaccessible c :=
id └──┘ └──┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ └──┘ ┴ ┴
doc └──┘ └──┘ ┴
482 ⟨h₁, ⟨le_of_lt h₁, le_antisymm (cof_ord_le _) h₂⟩,
483 ne_of_gt (lt_trans omega_pos h₁), h₃⟩
484
485 /- Lean's foundations prove the existence of ω many inaccessible
486 cardinals -/
487 theorem univ_inaccessible : is_inaccessible (univ.{u v}) :=
488 is_inaccessible.mk
489 (by simpa using lift_lt_univ' omega)
id └───┘
src └───┘
typ └───┘
doc └───┘
490 (by simp)
491 (λ c h, begin
id ┴
typ ┴
492 rcases lt_univ'.1 h with ⟨c, rfl⟩,
493 rw ← lift_two_power.{u (max (u+1) v)},
494 apply lift_lt_univ'
495 end)
st └─┘
496
497 theorem lt_power_cof {c : cardinal.{u}} : omega ≤ c → c < c ^ cof c.ord :=
id └──┘ └┘ └──┘ ┴ ┴└┘
src └──┘ └┘ └──┘ └┘
typ └──┘ └┘ └──┘ ┴ ┴└┘
doc └──┘ └┘ └──┘ └┘
498 quotient.induction_on c $ λ α h, begin
id ┴ ┴
typ ┴ ┴
499 rcases ord_eq α with ⟨r, wo, re⟩, resetI,
id ┴
typ ┴
500 have := ord_is_limit h,
501 rw [mk_def, re] at this ⊢,
502 rcases cof_eq' r this with ⟨S, H, Se⟩,
id ┴ └──┘
typ ┴ └──┘
503 have := sum_lt_prod (λ a:S, mk {x // r x a}) (λ _, mk α) (λ i, _),
id ┴ ┴ └┘ ┴
src └┘
typ ┴ ┴ └┘ ┴
doc └┘
504 { simp [Se.symm] at this ⊢,
505 refine lt_of_le_of_lt _ this,
506 refine ⟨embedding.of_surjective _⟩,
507 { exact λ x, x.2.1 },
st └┘
508 { exact λ a, let ⟨b, h, ab⟩ := H a in ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩ } },
id ┴ └┘
typ ┴ └┘
st └──┘
509 { have := typein_lt_type r i,
id ┴
typ ┴
510 rwa [← re, lt_ord] at this }
st └─
511 end
st ──┘
512
513 theorem lt_cof_power {a b : cardinal} (ha : omega ≤ a) (b1 : 1 < b) :
id └┘ └┘ └───┘ ┴ ┴
src └┘ └┘ └───┘
typ └┘ └┘ └───┘ ┴ ┴
doc └┘ └┘ └───┘
514 a < cof (b ^ a).ord :=
id ┴ ┴ ┴ └┘
src └┘
typ ┴ ┴ ┴ └┘
doc └┘
515 begin
516 have b0 : b ≠ 0 := ne_of_gt (lt_trans zero_lt_one b1),
id ┴
typ ┴
517 apply lt_imp_lt_of_le_imp_le (power_le_power_left $ power_ne_zero a b0),
id ┴
typ ┴
518 rw [power_mul, mul_eq_self ha],
519 exact lt_power_cof (le_trans ha $ le_of_lt $ cantor' _ b1),
520 end
st └─┘
521
522 end cardinal